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	|- ( aleph ` A ) e. On

Proof

Step	Hyp	Ref	Expression
1		alephfnon	|- aleph Fn On
2		fveq2	|- ( x = (/) -> ( aleph ` x ) = ( aleph ` (/) ) )
3	2	eleq1d	|- ( x = (/) -> ( ( aleph ` x ) e. On <-> ( aleph ` (/) ) e. On ) )
4		fveq2	|- ( x = y -> ( aleph ` x ) = ( aleph ` y ) )
5	4	eleq1d	|- ( x = y -> ( ( aleph ` x ) e. On <-> ( aleph ` y ) e. On ) )
6		fveq2	|- ( x = suc y -> ( aleph ` x ) = ( aleph ` suc y ) )
7	6	eleq1d	|- ( x = suc y -> ( ( aleph ` x ) e. On <-> ( aleph ` suc y ) e. On ) )
8		aleph0	|- ( aleph ` (/) ) = _om
9		omelon	|- _om e. On
10	8 9	eqeltri	|- ( aleph ` (/) ) e. On
11		alephsuc	|- ( y e. On -> ( aleph ` suc y ) = ( har ` ( aleph ` y ) ) )
12		harcl	|- ( har ` ( aleph ` y ) ) e. On
13	11 12	eqeltrdi	|- ( y e. On -> ( aleph ` suc y ) e. On )
14	13	a1d	|- ( y e. On -> ( ( aleph ` y ) e. On -> ( aleph ` suc y ) e. On ) )
15		vex	|- x e. _V
16		iunon	|- ( ( x e. _V /\ A. y e. x ( aleph ` y ) e. On ) -> U_ y e. x ( aleph ` y ) e. On )
17	15 16	mpan	|- ( A. y e. x ( aleph ` y ) e. On -> U_ y e. x ( aleph ` y ) e. On )
18		alephlim	|- ( ( x e. _V /\ Lim x ) -> ( aleph ` x ) = U_ y e. x ( aleph ` y ) )
19	15 18	mpan	|- ( Lim x -> ( aleph ` x ) = U_ y e. x ( aleph ` y ) )
20	19	eleq1d	|- ( Lim x -> ( ( aleph ` x ) e. On <-> U_ y e. x ( aleph ` y ) e. On ) )
21	17 20	imbitrrid	|- ( Lim x -> ( A. y e. x ( aleph ` y ) e. On -> ( aleph ` x ) e. On ) )
22	3 5 7 5 10 14 21	tfinds	|- ( y e. On -> ( aleph ` y ) e. On )
23	22	rgen	|- A. y e. On ( aleph ` y ) e. On
24		ffnfv	|- ( aleph : On --> On <-> ( aleph Fn On /\ A. y e. On ( aleph ` y ) e. On ) )
25	1 23 24	mpbir2an	|- aleph : On --> On
26		0elon	|- (/) e. On
27	25 26	f0cli	|- ( aleph ` A ) e. On