Metamath Proof Explorer

Theorem alephiso

Description: Aleph is an order isomorphism of the class of ordinal numbers onto the class of infinite cardinals. Definition 10.27 of TakeutiZaring p. 90. (Contributed by NM, 3-Aug-2004)

Ref Expression
Assertion alephiso 
|- aleph Isom _E , _E ( On , { x | ( _om C_ x /\ ( card ` x ) = x ) } )

Proof

Step Hyp Ref Expression
1 alephfnon 
 |-  aleph Fn On
2 isinfcard 
 |-  ( ( _om C_ x /\ ( card ` x ) = x ) <-> x e. ran aleph )
3 2 bicomi 
 |-  ( x e. ran aleph <-> ( _om C_ x /\ ( card ` x ) = x ) )
4 3 eqabi 
 |-  ran aleph = { x | ( _om C_ x /\ ( card ` x ) = x ) }
5 df-fo 
 |-  ( aleph : On -onto-> { x | ( _om C_ x /\ ( card ` x ) = x ) } <-> ( aleph Fn On /\ ran aleph = { x | ( _om C_ x /\ ( card ` x ) = x ) } ) )
6 1 4 5 mpbir2an 
 |-  aleph : On -onto-> { x | ( _om C_ x /\ ( card ` x ) = x ) }
7 fof 
 |-  ( aleph : On -onto-> { x | ( _om C_ x /\ ( card ` x ) = x ) } -> aleph : On --> { x | ( _om C_ x /\ ( card ` x ) = x ) } )
8 6 7 ax-mp 
 |-  aleph : On --> { x | ( _om C_ x /\ ( card ` x ) = x ) }
9 aleph11 
 |-  ( ( y e. On /\ z e. On ) -> ( ( aleph ` y ) = ( aleph ` z ) <-> y = z ) )
10 9 biimpd 
 |-  ( ( y e. On /\ z e. On ) -> ( ( aleph ` y ) = ( aleph ` z ) -> y = z ) )
11 10 rgen2 
 |-  A. y e. On A. z e. On ( ( aleph ` y ) = ( aleph ` z ) -> y = z )
12 dff13 
 |-  ( aleph : On -1-1-> { x | ( _om C_ x /\ ( card ` x ) = x ) } <-> ( aleph : On --> { x | ( _om C_ x /\ ( card ` x ) = x ) } /\ A. y e. On A. z e. On ( ( aleph ` y ) = ( aleph ` z ) -> y = z ) ) )
13 8 11 12 mpbir2an 
 |-  aleph : On -1-1-> { x | ( _om C_ x /\ ( card ` x ) = x ) }
14 df-f1o 
 |-  ( aleph : On -1-1-onto-> { x | ( _om C_ x /\ ( card ` x ) = x ) } <-> ( aleph : On -1-1-> { x | ( _om C_ x /\ ( card ` x ) = x ) } /\ aleph : On -onto-> { x | ( _om C_ x /\ ( card ` x ) = x ) } ) )
15 13 6 14 mpbir2an 
 |-  aleph : On -1-1-onto-> { x | ( _om C_ x /\ ( card ` x ) = x ) }
16 alephord2 
 |-  ( ( y e. On /\ z e. On ) -> ( y e. z <-> ( aleph ` y ) e. ( aleph ` z ) ) )
17 epel 
 |-  ( y _E z <-> y e. z )
18 fvex 
 |-  ( aleph ` z ) e. _V
19 18 epeli 
 |-  ( ( aleph ` y ) _E ( aleph ` z ) <-> ( aleph ` y ) e. ( aleph ` z ) )
20 16 17 19 3bitr4g 
 |-  ( ( y e. On /\ z e. On ) -> ( y _E z <-> ( aleph ` y ) _E ( aleph ` z ) ) )
21 20 rgen2 
 |-  A. y e. On A. z e. On ( y _E z <-> ( aleph ` y ) _E ( aleph ` z ) )
22 df-isom 
 |-  ( aleph Isom _E , _E ( On , { x | ( _om C_ x /\ ( card ` x ) = x ) } ) <-> ( aleph : On -1-1-onto-> { x | ( _om C_ x /\ ( card ` x ) = x ) } /\ A. y e. On A. z e. On ( y _E z <-> ( aleph ` y ) _E ( aleph ` z ) ) ) )
23 15 21 22 mpbir2an 
 |-  aleph Isom _E , _E ( On , { x | ( _om C_ x /\ ( card ` x ) = x ) } )