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
|- ( 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 syl5ibr
 |-  ( 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