This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ℵ ‘ 𝐴 ) ∈ On

Proof

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