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