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	abbi2i	|- 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 ) } )