MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  alephon Structured version   Visualization version   GIF version

Theorem alephon 9688
Description: An aleph is an ordinal number. (Contributed by NM, 10-Nov-2003.) (Revised by Mario Carneiro, 13-Sep-2013.)
Assertion
Ref Expression
alephon (ℵ‘𝐴) ∈ On

Proof of Theorem alephon
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 alephfnon 9684 . . 3 ℵ Fn On
2 fveq2 6722 . . . . . 6 (𝑥 = ∅ → (ℵ‘𝑥) = (ℵ‘∅))
32eleq1d 2822 . . . . 5 (𝑥 = ∅ → ((ℵ‘𝑥) ∈ On ↔ (ℵ‘∅) ∈ On))
4 fveq2 6722 . . . . . 6 (𝑥 = 𝑦 → (ℵ‘𝑥) = (ℵ‘𝑦))
54eleq1d 2822 . . . . 5 (𝑥 = 𝑦 → ((ℵ‘𝑥) ∈ On ↔ (ℵ‘𝑦) ∈ On))
6 fveq2 6722 . . . . . 6 (𝑥 = suc 𝑦 → (ℵ‘𝑥) = (ℵ‘suc 𝑦))
76eleq1d 2822 . . . . 5 (𝑥 = suc 𝑦 → ((ℵ‘𝑥) ∈ On ↔ (ℵ‘suc 𝑦) ∈ On))
8 aleph0 9685 . . . . . 6 (ℵ‘∅) = ω
9 omelon 9266 . . . . . 6 ω ∈ On
108, 9eqeltri 2834 . . . . 5 (ℵ‘∅) ∈ On
11 alephsuc 9687 . . . . . . 7 (𝑦 ∈ On → (ℵ‘suc 𝑦) = (har‘(ℵ‘𝑦)))
12 harcl 9180 . . . . . . 7 (har‘(ℵ‘𝑦)) ∈ On
1311, 12eqeltrdi 2846 . . . . . 6 (𝑦 ∈ On → (ℵ‘suc 𝑦) ∈ On)
1413a1d 25 . . . . 5 (𝑦 ∈ On → ((ℵ‘𝑦) ∈ On → (ℵ‘suc 𝑦) ∈ On))
15 vex 3417 . . . . . . 7 𝑥 ∈ V
16 iunon 8081 . . . . . . 7 ((𝑥 ∈ V ∧ ∀𝑦𝑥 (ℵ‘𝑦) ∈ On) → 𝑦𝑥 (ℵ‘𝑦) ∈ On)
1715, 16mpan 690 . . . . . 6 (∀𝑦𝑥 (ℵ‘𝑦) ∈ On → 𝑦𝑥 (ℵ‘𝑦) ∈ On)
18 alephlim 9686 . . . . . . . 8 ((𝑥 ∈ V ∧ Lim 𝑥) → (ℵ‘𝑥) = 𝑦𝑥 (ℵ‘𝑦))
1915, 18mpan 690 . . . . . . 7 (Lim 𝑥 → (ℵ‘𝑥) = 𝑦𝑥 (ℵ‘𝑦))
2019eleq1d 2822 . . . . . 6 (Lim 𝑥 → ((ℵ‘𝑥) ∈ On ↔ 𝑦𝑥 (ℵ‘𝑦) ∈ On))
2117, 20syl5ibr 249 . . . . 5 (Lim 𝑥 → (∀𝑦𝑥 (ℵ‘𝑦) ∈ On → (ℵ‘𝑥) ∈ On))
223, 5, 7, 5, 10, 14, 21tfinds 7643 . . . 4 (𝑦 ∈ On → (ℵ‘𝑦) ∈ On)
2322rgen 3071 . . 3 𝑦 ∈ On (ℵ‘𝑦) ∈ On
24 ffnfv 6940 . . 3 (ℵ:On⟶On ↔ (ℵ Fn On ∧ ∀𝑦 ∈ On (ℵ‘𝑦) ∈ On))
251, 23, 24mpbir2an 711 . 2 ℵ:On⟶On
26 0elon 6271 . 2 ∅ ∈ On
2725, 26f0cli 6922 1 (ℵ‘𝐴) ∈ On
Colors of variables: wff setvar class
Syntax hints:   = wceq 1543  wcel 2110  wral 3061  Vcvv 3413  c0 4242   ciun 4909  Oncon0 6218  Lim wlim 6219  suc csuc 6220   Fn wfn 6380  wf 6381  cfv 6385  ωcom 7649  harchar 9177  cale 9557
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5184  ax-sep 5197  ax-nul 5204  ax-pow 5263  ax-pr 5327  ax-un 7528  ax-inf2 9261
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3415  df-sbc 3700  df-csb 3817  df-dif 3874  df-un 3876  df-in 3878  df-ss 3888  df-pss 3890  df-nul 4243  df-if 4445  df-pw 4520  df-sn 4547  df-pr 4549  df-tp 4551  df-op 4553  df-uni 4825  df-iun 4911  df-br 5059  df-opab 5121  df-mpt 5141  df-tr 5167  df-id 5460  df-eprel 5465  df-po 5473  df-so 5474  df-fr 5514  df-se 5515  df-we 5516  df-xp 5562  df-rel 5563  df-cnv 5564  df-co 5565  df-dm 5566  df-rn 5567  df-res 5568  df-ima 5569  df-pred 6165  df-ord 6221  df-on 6222  df-lim 6223  df-suc 6224  df-iota 6343  df-fun 6387  df-fn 6388  df-f 6389  df-f1 6390  df-fo 6391  df-f1o 6392  df-fv 6393  df-isom 6394  df-riota 7175  df-om 7650  df-wrecs 8052  df-recs 8113  df-rdg 8151  df-en 8632  df-dom 8633  df-oi 9131  df-har 9178  df-aleph 9561
This theorem is referenced by:  alephnbtwn  9690  alephnbtwn2  9691  alephordilem1  9692  alephord  9694  alephord2  9695  alephord3  9697  alephsucdom  9698  alephsuc2  9699  alephf1  9704  alephsdom  9705  alephdom2  9706  alephle  9707  cardaleph  9708  alephf1ALT  9722  alephfp  9727  dfac12k  9766  alephsing  9895  alephval2  10191  alephadd  10196  alephmul  10197  alephexp1  10198  alephsuc3  10199  alephreg  10201  pwcfsdom  10202  cfpwsdom  10203  gchaleph  10290  gchaleph2  10291  gch2  10294  alephiso2  40849
  Copyright terms: Public domain W3C validator