Theorem alephgeom 4902

Description: Every aleph is greater than or equal to the set of natural numbers.

Assertion

Ref	Expression
alephgeom	⊢ (A ∈ On ↔ ω ⊆ (ℵ ‘A))

Proof of Theorem alephgeom

Step	Hyp	Ref	Expression
1		0ss 2313	. . . 4 ⊢ ∅ ⊆ A
2		0elon 3038	. . . . 5 ⊢ ∅ ∈ On
3		alephord3 4898	. . . . 5 ⊢ ((∅ ∈ On ⋀ A ∈ On) → (∅ ⊆ A ↔ (ℵ ‘∅) ⊆ (ℵ ‘A)))
4	2, 3	mpan 699	. . . 4 ⊢ (A ∈ On → (∅ ⊆ A ↔ (ℵ ‘∅) ⊆ (ℵ ‘A)))
5	1, 4	mpbii 193	. . 3 ⊢ (A ∈ On → (ℵ ‘∅) ⊆ (ℵ ‘A))
6		aleph0 4883	. . 3 ⊢ (ℵ ‘∅) = ω
7	5, 6	syl5ssr 2117	. 2 ⊢ (A ∈ On → ω ⊆ (ℵ ‘A))
8		peano1 3165	. . . . . 6 ⊢ ∅ ∈ ω
9		ordom 3157	. . . . . . . 8 ⊢ Ord ω
10		ord0 3037	. . . . . . . 8 ⊢ Ord ∅
11		ordtri1 2996	. . . . . . . 8 ⊢ ((Ord ω ⋀ Ord ∅) → (ω ⊆ ∅ ↔ ¬ ∅ ∈ ω))
12	9, 10, 11	mp2an 701	. . . . . . 7 ⊢ (ω ⊆ ∅ ↔ ¬ ∅ ∈ ω)
13	12	con2bii 221	. . . . . 6 ⊢ (∅ ∈ ω ↔ ¬ ω ⊆ ∅)
14	8, 13	mpbi 189	. . . . 5 ⊢ ¬ ω ⊆ ∅
15		ndmfv 3761	. . . . . 6 ⊢ (¬ A ∈ dom ℵ → (ℵ ‘A) = ∅)
16	15	sseq2d 2100	. . . . 5 ⊢ (¬ A ∈ dom ℵ → (ω ⊆ (ℵ ‘A) ↔ ω ⊆ ∅))
17	14, 16	mtbiri 721	. . . 4 ⊢ (¬ A ∈ dom ℵ → ¬ ω ⊆ (ℵ ‘A))
18	17	a3i 74	. . 3 ⊢ (ω ⊆ (ℵ ‘A) → A ∈ dom ℵ)
19		alephfnon 4882	. . . 4 ⊢ ℵ Fn On
20		fndm 3603	. . . 4 ⊢ (ℵ Fn On → dom ℵ = On)
21	19, 20	ax-mp 7	. . 3 ⊢ dom ℵ = On
22	18, 21	syl6eleq 1565	. 2 ⊢ (ω ⊆ (ℵ ‘A) → A ∈ On)
23	7, 22	impbii 157	1 ⊢ (A ∈ On ↔ ω ⊆ (ℵ ‘A))

Syntax hints:  ¬ wn 2   ↔ wb 146   = wceq 960   ∈ wcel 962   ⊆ wss 2058  ∅c0 2291  Ord word 2963  Oncon0 2964  ωcom 3147  dom cdm 3186   Fn wfn 3193   ‘cfv 3198  ℵcale 4831

This theorem is referenced by:  alephislim 4903  cardalephex 4906  isinfcard 4907  alephval2 4922  alephval3 4923  alephadd 7615  alephmul 7616  alephexp1 7617  alephsuc3 7618  alephexp2 7619

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-9 969  ax-10 970  ax-11 971  ax-12 972  ax-13 973  ax-14 974  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1127  ax-10o 1144  ax-16 1214  ax-11o 1222  ax-ext 1464  ax-rep 2708  ax-sep 2718  ax-nul 2725  ax-pow 2758  ax-pr 2795  ax-un 2882  ax-reg 4608  ax-inf2 4642  ax-ac 4761

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 780  df-3an 781  df-ex 985  df-sb 1176  df-eu 1386  df-mo 1387  df-clab 1470  df-cleq 1475  df-clel 1478  df-ne 1594  df-ral 1656  df-rex 1657  df-reu 1658  df-rab 1659  df-v 1819  df-sbc 1949  df-dif 2060  df-un 2061  df-in 2062  df-ss 2064  df-pss 2066  df-nul 2292  df-if 2374  df-pw 2414  df-sn 2424  df-pr 2425  df-tp 2427  df-op 2428  df-uni 2518  df-int 2548  df-iun 2582  df-br 2635  df-opab 2682  df-tr 2696  df-eprel 2848  df-id 2851  df-po 2856  df-so 2866  df-fr 2933  df-we 2950  df-ord 2967  df-on 2968  df-lim 2969  df-suc 2970  df-om 3148  df-xp 3200  df-rel 3201  df-cnv 3202  df-co 3203  df-dm 3204  df-rn 3205  df-res 3206  df-ima 3207  df-fun 3208  df-fn 3209  df-f 3210  df-f1 3211  df-fo 3212  df-f1o 3213  df-fv 3214  df-rdg 3948  df-er 4277  df-en 4386  df-dom 4387  df-sdom 4388  df-fin 4389  df-card 4833  df-aleph 4834

Copyright terms: Public domain