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