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 )