Metamath Proof Explorer

Theorem alephon

Description: An aleph is an ordinal number. (Contributed by NM, 10-Nov-2003) (Revised by Mario Carneiro, 13-Sep-2013)

Ref Expression
Assertion alephon ⊢ℵ⁡A∈On

Proof

Step Hyp Ref Expression
1 alephfnon ⊢ℵFnOn
2 fveq2 ⊢x=∅→ℵ⁡x=ℵ⁡∅
3 2 eleq1d ⊢x=∅→ℵ⁡x∈On↔ℵ⁡∅∈On
4 fveq2 ⊢x=y→ℵ⁡x=ℵ⁡y
5 4 eleq1d ⊢x=y→ℵ⁡x∈On↔ℵ⁡y∈On
6 fveq2 ⊢x=suc⁡y→ℵ⁡x=ℵ⁡suc⁡y
7 6 eleq1d ⊢x=suc⁡y→ℵ⁡x∈On↔ℵ⁡suc⁡y∈On
8 aleph0 ⊢ℵ⁡∅=ω
9 omelon ⊢ω∈On
10 8 9 eqeltri ⊢ℵ⁡∅∈On
11 alephsuc ⊢y∈On→ℵ⁡suc⁡y=har⁡ℵ⁡y
12 harcl ⊢har⁡ℵ⁡y∈On
13 11 12 eqeltrdi ⊢y∈On→ℵ⁡suc⁡y∈On
14 13 a1d ⊢y∈On→ℵ⁡y∈On→ℵ⁡suc⁡y∈On
15 vex ⊢x∈V
16 iunon ⊢x∈V∧∀y∈xℵ⁡y∈On→⋃y∈xℵ⁡y∈On
17 15 16 mpan ⊢∀y∈xℵ⁡y∈On→⋃y∈xℵ⁡y∈On
18 alephlim ⊢x∈V∧Lim⁡x→ℵ⁡x=⋃y∈xℵ⁡y
19 15 18 mpan ⊢Lim⁡x→ℵ⁡x=⋃y∈xℵ⁡y
20 19 eleq1d ⊢Lim⁡x→ℵ⁡x∈On↔⋃y∈xℵ⁡y∈On
21 17 20 imbitrrid ⊢Lim⁡x→∀y∈xℵ⁡y∈On→ℵ⁡x∈On
22 3 5 7 5 10 14 21 tfinds ⊢y∈On→ℵ⁡y∈On
23 22 rgen ⊢∀y∈Onℵ⁡y∈On
24 ffnfv ⊢ℵ:On⟶On↔ℵFnOn∧∀y∈Onℵ⁡y∈On
25 1 23 24 mpbir2an ⊢ℵ:On⟶On
26 0elon ⊢∅∈On
27 25 26 f0cli ⊢ℵ⁡A∈On