Metamath Proof Explorer

Theorem xporderlem

Description: Lemma for lexicographical ordering theorems. (Contributed by Scott Fenton, 16-Mar-2011)

Ref Expression
Hypothesis xporderlem.1 
|- T = { <. x , y >. | ( ( x e. ( A X. B ) /\ y e. ( A X. B ) ) /\ ( ( 1st ` x ) R ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) S ( 2nd ` y ) ) ) ) }
Assertion xporderlem 
|- ( <. a , b >. T <. c , d >. <-> ( ( ( a e. A /\ c e. A ) /\ ( b e. B /\ d e. B ) ) /\ ( a R c \/ ( a = c /\ b S d ) ) ) )

Proof

Step Hyp Ref Expression
1 xporderlem.1 
 |-  T = { <. x , y >. | ( ( x e. ( A X. B ) /\ y e. ( A X. B ) ) /\ ( ( 1st ` x ) R ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) S ( 2nd ` y ) ) ) ) }
2 df-br 
 |-  ( <. a , b >. T <. c , d >. <-> <. <. a , b >. , <. c , d >. >. e. T )
3 1 eleq2i 
 |-  ( <. <. a , b >. , <. c , d >. >. e. T <-> <. <. a , b >. , <. c , d >. >. e. { <. x , y >. | ( ( x e. ( A X. B ) /\ y e. ( A X. B ) ) /\ ( ( 1st ` x ) R ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) S ( 2nd ` y ) ) ) ) } )
4 2 3 bitri 
 |-  ( <. a , b >. T <. c , d >. <-> <. <. a , b >. , <. c , d >. >. e. { <. x , y >. | ( ( x e. ( A X. B ) /\ y e. ( A X. B ) ) /\ ( ( 1st ` x ) R ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) S ( 2nd ` y ) ) ) ) } )
5 opex 
 |-  <. a , b >. e. _V
6 opex 
 |-  <. c , d >. e. _V
7 eleq1 
 |-  ( x = <. a , b >. -> ( x e. ( A X. B ) <-> <. a , b >. e. ( A X. B ) ) )
8 opelxp 
 |-  ( <. a , b >. e. ( A X. B ) <-> ( a e. A /\ b e. B ) )
9 7 8 bitrdi 
 |-  ( x = <. a , b >. -> ( x e. ( A X. B ) <-> ( a e. A /\ b e. B ) ) )
10 9 anbi1d 
 |-  ( x = <. a , b >. -> ( ( x e. ( A X. B ) /\ y e. ( A X. B ) ) <-> ( ( a e. A /\ b e. B ) /\ y e. ( A X. B ) ) ) )
11 vex 
 |-  a e. _V
12 vex 
 |-  b e. _V
13 11 12 op1std 
 |-  ( x = <. a , b >. -> ( 1st ` x ) = a )
14 13 breq1d 
 |-  ( x = <. a , b >. -> ( ( 1st ` x ) R ( 1st ` y ) <-> a R ( 1st ` y ) ) )
15 13 eqeq1d 
 |-  ( x = <. a , b >. -> ( ( 1st ` x ) = ( 1st ` y ) <-> a = ( 1st ` y ) ) )
16 11 12 op2ndd 
 |-  ( x = <. a , b >. -> ( 2nd ` x ) = b )
17 16 breq1d 
 |-  ( x = <. a , b >. -> ( ( 2nd ` x ) S ( 2nd ` y ) <-> b S ( 2nd ` y ) ) )
18 15 17 anbi12d 
 |-  ( x = <. a , b >. -> ( ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) S ( 2nd ` y ) ) <-> ( a = ( 1st ` y ) /\ b S ( 2nd ` y ) ) ) )
19 14 18 orbi12d 
 |-  ( x = <. a , b >. -> ( ( ( 1st ` x ) R ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) S ( 2nd ` y ) ) ) <-> ( a R ( 1st ` y ) \/ ( a = ( 1st ` y ) /\ b S ( 2nd ` y ) ) ) ) )
20 10 19 anbi12d 
 |-  ( x = <. a , b >. -> ( ( ( x e. ( A X. B ) /\ y e. ( A X. B ) ) /\ ( ( 1st ` x ) R ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) S ( 2nd ` y ) ) ) ) <-> ( ( ( a e. A /\ b e. B ) /\ y e. ( A X. B ) ) /\ ( a R ( 1st ` y ) \/ ( a = ( 1st ` y ) /\ b S ( 2nd ` y ) ) ) ) ) )
21 eleq1 
 |-  ( y = <. c , d >. -> ( y e. ( A X. B ) <-> <. c , d >. e. ( A X. B ) ) )
22 opelxp 
 |-  ( <. c , d >. e. ( A X. B ) <-> ( c e. A /\ d e. B ) )
23 21 22 bitrdi 
 |-  ( y = <. c , d >. -> ( y e. ( A X. B ) <-> ( c e. A /\ d e. B ) ) )
24 23 anbi2d 
 |-  ( y = <. c , d >. -> ( ( ( a e. A /\ b e. B ) /\ y e. ( A X. B ) ) <-> ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) ) ) )
25 vex 
 |-  c e. _V
26 vex 
 |-  d e. _V
27 25 26 op1std 
 |-  ( y = <. c , d >. -> ( 1st ` y ) = c )
28 27 breq2d 
 |-  ( y = <. c , d >. -> ( a R ( 1st ` y ) <-> a R c ) )
29 27 eqeq2d 
 |-  ( y = <. c , d >. -> ( a = ( 1st ` y ) <-> a = c ) )
30 25 26 op2ndd 
 |-  ( y = <. c , d >. -> ( 2nd ` y ) = d )
31 30 breq2d 
 |-  ( y = <. c , d >. -> ( b S ( 2nd ` y ) <-> b S d ) )
32 29 31 anbi12d 
 |-  ( y = <. c , d >. -> ( ( a = ( 1st ` y ) /\ b S ( 2nd ` y ) ) <-> ( a = c /\ b S d ) ) )
33 28 32 orbi12d 
 |-  ( y = <. c , d >. -> ( ( a R ( 1st ` y ) \/ ( a = ( 1st ` y ) /\ b S ( 2nd ` y ) ) ) <-> ( a R c \/ ( a = c /\ b S d ) ) ) )
34 24 33 anbi12d 
 |-  ( y = <. c , d >. -> ( ( ( ( a e. A /\ b e. B ) /\ y e. ( A X. B ) ) /\ ( a R ( 1st ` y ) \/ ( a = ( 1st ` y ) /\ b S ( 2nd ` y ) ) ) ) <-> ( ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) ) /\ ( a R c \/ ( a = c /\ b S d ) ) ) ) )
35 5 6 20 34 opelopab 
 |-  ( <. <. a , b >. , <. c , d >. >. e. { <. x , y >. | ( ( x e. ( A X. B ) /\ y e. ( A X. B ) ) /\ ( ( 1st ` x ) R ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) S ( 2nd ` y ) ) ) ) } <-> ( ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) ) /\ ( a R c \/ ( a = c /\ b S d ) ) ) )
36 an4 
 |-  ( ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) ) <-> ( ( a e. A /\ c e. A ) /\ ( b e. B /\ d e. B ) ) )
37 36 anbi1i 
 |-  ( ( ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) ) /\ ( a R c \/ ( a = c /\ b S d ) ) ) <-> ( ( ( a e. A /\ c e. A ) /\ ( b e. B /\ d e. B ) ) /\ ( a R c \/ ( a = c /\ b S d ) ) ) )
38 4 35 37 3bitri 
 |-  ( <. a , b >. T <. c , d >. <-> ( ( ( a e. A /\ c e. A ) /\ ( b e. B /\ d e. B ) ) /\ ( a R c \/ ( a = c /\ b S d ) ) ) )