This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem infxpen

Description: Every infinite ordinal is equinumerous to its Cartesian square. Proposition 10.39 of TakeutiZaring p. 94, whose proof we follow closely. The key idea is to show that the relation R is a well-ordering of ( On X. On ) with the additional property that R -initial segments of ( x X. x ) (where x is a limit ordinal) are of cardinality at most x . (Contributed by Mario Carneiro, 9-Mar-2013) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Assertion infxpen 
|- ( ( A e. On /\ _om C_ A ) -> ( A X. A ) ~~ A )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( 1st ` x ) e. ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) ) ) } = { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( 1st ` x ) e. ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) ) ) }
2 eleq1w 
 |-  ( s = z -> ( s e. ( On X. On ) <-> z e. ( On X. On ) ) )
3 eleq1w 
 |-  ( t = w -> ( t e. ( On X. On ) <-> w e. ( On X. On ) ) )
4 2 3 bi2anan9 
 |-  ( ( s = z /\ t = w ) -> ( ( s e. ( On X. On ) /\ t e. ( On X. On ) ) <-> ( z e. ( On X. On ) /\ w e. ( On X. On ) ) ) )
5 fveq2 
 |-  ( s = z -> ( 1st ` s ) = ( 1st ` z ) )
6 fveq2 
 |-  ( s = z -> ( 2nd ` s ) = ( 2nd ` z ) )
7 5 6 uneq12d 
 |-  ( s = z -> ( ( 1st ` s ) u. ( 2nd ` s ) ) = ( ( 1st ` z ) u. ( 2nd ` z ) ) )
8 7 adantr 
 |-  ( ( s = z /\ t = w ) -> ( ( 1st ` s ) u. ( 2nd ` s ) ) = ( ( 1st ` z ) u. ( 2nd ` z ) ) )
9 fveq2 
 |-  ( t = w -> ( 1st ` t ) = ( 1st ` w ) )
10 fveq2 
 |-  ( t = w -> ( 2nd ` t ) = ( 2nd ` w ) )
11 9 10 uneq12d 
 |-  ( t = w -> ( ( 1st ` t ) u. ( 2nd ` t ) ) = ( ( 1st ` w ) u. ( 2nd ` w ) ) )
12 11 adantl 
 |-  ( ( s = z /\ t = w ) -> ( ( 1st ` t ) u. ( 2nd ` t ) ) = ( ( 1st ` w ) u. ( 2nd ` w ) ) )
13 8 12 eleq12d 
 |-  ( ( s = z /\ t = w ) -> ( ( ( 1st ` s ) u. ( 2nd ` s ) ) e. ( ( 1st ` t ) u. ( 2nd ` t ) ) <-> ( ( 1st ` z ) u. ( 2nd ` z ) ) e. ( ( 1st ` w ) u. ( 2nd ` w ) ) ) )
14 7 11 eqeqan12d 
 |-  ( ( s = z /\ t = w ) -> ( ( ( 1st ` s ) u. ( 2nd ` s ) ) = ( ( 1st ` t ) u. ( 2nd ` t ) ) <-> ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( ( 1st ` w ) u. ( 2nd ` w ) ) ) )
15 breq12 
 |-  ( ( s = z /\ t = w ) -> ( s { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( 1st ` x ) e. ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) ) ) } t <-> z { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( 1st ` x ) e. ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) ) ) } w ) )
16 14 15 anbi12d 
 |-  ( ( s = z /\ t = w ) -> ( ( ( ( 1st ` s ) u. ( 2nd ` s ) ) = ( ( 1st ` t ) u. ( 2nd ` t ) ) /\ s { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( 1st ` x ) e. ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) ) ) } t ) <-> ( ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( ( 1st ` w ) u. ( 2nd ` w ) ) /\ z { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( 1st ` x ) e. ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) ) ) } w ) ) )
17 13 16 orbi12d 
 |-  ( ( s = z /\ t = w ) -> ( ( ( ( 1st ` s ) u. ( 2nd ` s ) ) e. ( ( 1st ` t ) u. ( 2nd ` t ) ) \/ ( ( ( 1st ` s ) u. ( 2nd ` s ) ) = ( ( 1st ` t ) u. ( 2nd ` t ) ) /\ s { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( 1st ` x ) e. ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) ) ) } t ) ) <-> ( ( ( 1st ` z ) u. ( 2nd ` z ) ) e. ( ( 1st ` w ) u. ( 2nd ` w ) ) \/ ( ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( ( 1st ` w ) u. ( 2nd ` w ) ) /\ z { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( 1st ` x ) e. ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) ) ) } w ) ) ) )
18 4 17 anbi12d 
 |-  ( ( s = z /\ t = w ) -> ( ( ( s e. ( On X. On ) /\ t e. ( On X. On ) ) /\ ( ( ( 1st ` s ) u. ( 2nd ` s ) ) e. ( ( 1st ` t ) u. ( 2nd ` t ) ) \/ ( ( ( 1st ` s ) u. ( 2nd ` s ) ) = ( ( 1st ` t ) u. ( 2nd ` t ) ) /\ s { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( 1st ` x ) e. ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) ) ) } t ) ) ) <-> ( ( z e. ( On X. On ) /\ w e. ( On X. On ) ) /\ ( ( ( 1st ` z ) u. ( 2nd ` z ) ) e. ( ( 1st ` w ) u. ( 2nd ` w ) ) \/ ( ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( ( 1st ` w ) u. ( 2nd ` w ) ) /\ z { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( 1st ` x ) e. ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) ) ) } w ) ) ) ) )
19 18 cbvopabv 
 |-  { <. s , t >. | ( ( s e. ( On X. On ) /\ t e. ( On X. On ) ) /\ ( ( ( 1st ` s ) u. ( 2nd ` s ) ) e. ( ( 1st ` t ) u. ( 2nd ` t ) ) \/ ( ( ( 1st ` s ) u. ( 2nd ` s ) ) = ( ( 1st ` t ) u. ( 2nd ` t ) ) /\ s { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( 1st ` x ) e. ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) ) ) } t ) ) ) } = { <. z , w >. | ( ( z e. ( On X. On ) /\ w e. ( On X. On ) ) /\ ( ( ( 1st ` z ) u. ( 2nd ` z ) ) e. ( ( 1st ` w ) u. ( 2nd ` w ) ) \/ ( ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( ( 1st ` w ) u. ( 2nd ` w ) ) /\ z { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( 1st ` x ) e. ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) ) ) } w ) ) ) }
20 eqid 
 |-  ( { <. s , t >. | ( ( s e. ( On X. On ) /\ t e. ( On X. On ) ) /\ ( ( ( 1st ` s ) u. ( 2nd ` s ) ) e. ( ( 1st ` t ) u. ( 2nd ` t ) ) \/ ( ( ( 1st ` s ) u. ( 2nd ` s ) ) = ( ( 1st ` t ) u. ( 2nd ` t ) ) /\ s { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( 1st ` x ) e. ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) ) ) } t ) ) ) } i^i ( ( a X. a ) X. ( a X. a ) ) ) = ( { <. s , t >. | ( ( s e. ( On X. On ) /\ t e. ( On X. On ) ) /\ ( ( ( 1st ` s ) u. ( 2nd ` s ) ) e. ( ( 1st ` t ) u. ( 2nd ` t ) ) \/ ( ( ( 1st ` s ) u. ( 2nd ` s ) ) = ( ( 1st ` t ) u. ( 2nd ` t ) ) /\ s { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( 1st ` x ) e. ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) ) ) } t ) ) ) } i^i ( ( a X. a ) X. ( a X. a ) ) )
21 biid 
 |-  ( ( ( a e. On /\ A. m e. a ( _om C_ m -> ( m X. m ) ~~ m ) ) /\ ( _om C_ a /\ A. m e. a m ~< a ) ) <-> ( ( a e. On /\ A. m e. a ( _om C_ m -> ( m X. m ) ~~ m ) ) /\ ( _om C_ a /\ A. m e. a m ~< a ) ) )
22 eqid 
 |-  ( ( 1st ` w ) u. ( 2nd ` w ) ) = ( ( 1st ` w ) u. ( 2nd ` w ) )
23 eqid 
 |-  OrdIso ( ( { <. s , t >. | ( ( s e. ( On X. On ) /\ t e. ( On X. On ) ) /\ ( ( ( 1st ` s ) u. ( 2nd ` s ) ) e. ( ( 1st ` t ) u. ( 2nd ` t ) ) \/ ( ( ( 1st ` s ) u. ( 2nd ` s ) ) = ( ( 1st ` t ) u. ( 2nd ` t ) ) /\ s { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( 1st ` x ) e. ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) ) ) } t ) ) ) } i^i ( ( a X. a ) X. ( a X. a ) ) ) , ( a X. a ) ) = OrdIso ( ( { <. s , t >. | ( ( s e. ( On X. On ) /\ t e. ( On X. On ) ) /\ ( ( ( 1st ` s ) u. ( 2nd ` s ) ) e. ( ( 1st ` t ) u. ( 2nd ` t ) ) \/ ( ( ( 1st ` s ) u. ( 2nd ` s ) ) = ( ( 1st ` t ) u. ( 2nd ` t ) ) /\ s { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( 1st ` x ) e. ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) ) ) } t ) ) ) } i^i ( ( a X. a ) X. ( a X. a ) ) ) , ( a X. a ) )
24 1 19 20 21 22 23 infxpenlem 
 |-  ( ( A e. On /\ _om C_ A ) -> ( A X. A ) ~~ A )