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 ⊢ ℵ Fn On
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 syl5ibr ⊢ 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 ↔ ℵ Fn On ∧ ∀ y ∈ On ℵ ⁡ y ∈ On
25 1 23 24 mpbir2an ⊢ ℵ : On ⟶ On
26 0elon ⊢ ∅ ∈ On
27 25 26 f0cli ⊢ ℵ ⁡ A ∈ On