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