Metamath Proof Explorer

Theorem xpord2lem

Description: Lemma for cross product ordering. Calculate the value of the cross product relationship. (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Hypothesis xpord2.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 ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) /\ x =/= y ) ) }
Assertion xpord2lem 
|- ( <. a , b >. T <. c , d >. <-> ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) /\ ( ( a R c \/ a = c ) /\ ( b S d \/ b = d ) /\ ( a =/= c \/ b =/= d ) ) ) )

Proof

Step Hyp Ref Expression
1 xpord2.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 ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) /\ x =/= y ) ) }
2 opex 
 |-  <. a , b >. e. _V
3 opex 
 |-  <. c , d >. e. _V
4 eleq1 
 |-  ( x = <. a , b >. -> ( x e. ( A X. B ) <-> <. a , b >. e. ( A X. B ) ) )
5 opelxp 
 |-  ( <. a , b >. e. ( A X. B ) <-> ( a e. A /\ b e. B ) )
6 4 5 bitrdi 
 |-  ( x = <. a , b >. -> ( x e. ( A X. B ) <-> ( a e. A /\ b e. B ) ) )
7 vex 
 |-  a e. _V
8 vex 
 |-  b e. _V
9 7 8 op1std 
 |-  ( x = <. a , b >. -> ( 1st ` x ) = a )
10 9 breq1d 
 |-  ( x = <. a , b >. -> ( ( 1st ` x ) R ( 1st ` y ) <-> a R ( 1st ` y ) ) )
11 9 eqeq1d 
 |-  ( x = <. a , b >. -> ( ( 1st ` x ) = ( 1st ` y ) <-> a = ( 1st ` y ) ) )
12 10 11 orbi12d 
 |-  ( x = <. a , b >. -> ( ( ( 1st ` x ) R ( 1st ` y ) \/ ( 1st ` x ) = ( 1st ` y ) ) <-> ( a R ( 1st ` y ) \/ a = ( 1st ` y ) ) ) )
13 7 8 op2ndd 
 |-  ( x = <. a , b >. -> ( 2nd ` x ) = b )
14 13 breq1d 
 |-  ( x = <. a , b >. -> ( ( 2nd ` x ) S ( 2nd ` y ) <-> b S ( 2nd ` y ) ) )
15 13 eqeq1d 
 |-  ( x = <. a , b >. -> ( ( 2nd ` x ) = ( 2nd ` y ) <-> b = ( 2nd ` y ) ) )
16 14 15 orbi12d 
 |-  ( x = <. a , b >. -> ( ( ( 2nd ` x ) S ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) <-> ( b S ( 2nd ` y ) \/ b = ( 2nd ` y ) ) ) )
17 neeq1 
 |-  ( x = <. a , b >. -> ( x =/= y <-> <. a , b >. =/= y ) )
18 12 16 17 3anbi123d 
 |-  ( x = <. a , b >. -> ( ( ( ( 1st ` x ) R ( 1st ` y ) \/ ( 1st ` x ) = ( 1st ` y ) ) /\ ( ( 2nd ` x ) S ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) /\ x =/= y ) <-> ( ( a R ( 1st ` y ) \/ a = ( 1st ` y ) ) /\ ( b S ( 2nd ` y ) \/ b = ( 2nd ` y ) ) /\ <. a , b >. =/= y ) ) )
19 6 18 3anbi13d 
 |-  ( 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 ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) /\ x =/= y ) ) <-> ( ( a e. A /\ b e. B ) /\ y e. ( A X. B ) /\ ( ( a R ( 1st ` y ) \/ a = ( 1st ` y ) ) /\ ( b S ( 2nd ` y ) \/ b = ( 2nd ` y ) ) /\ <. a , b >. =/= y ) ) ) )
20 eleq1 
 |-  ( y = <. c , d >. -> ( y e. ( A X. B ) <-> <. c , d >. e. ( A X. B ) ) )
21 opelxp 
 |-  ( <. c , d >. e. ( A X. B ) <-> ( c e. A /\ d e. B ) )
22 20 21 bitrdi 
 |-  ( y = <. c , d >. -> ( y e. ( A X. B ) <-> ( c e. A /\ d e. B ) ) )
23 vex 
 |-  c e. _V
24 vex 
 |-  d e. _V
25 23 24 op1std 
 |-  ( y = <. c , d >. -> ( 1st ` y ) = c )
26 25 breq2d 
 |-  ( y = <. c , d >. -> ( a R ( 1st ` y ) <-> a R c ) )
27 25 eqeq2d 
 |-  ( y = <. c , d >. -> ( a = ( 1st ` y ) <-> a = c ) )
28 26 27 orbi12d 
 |-  ( y = <. c , d >. -> ( ( a R ( 1st ` y ) \/ a = ( 1st ` y ) ) <-> ( a R c \/ a = c ) ) )
29 23 24 op2ndd 
 |-  ( y = <. c , d >. -> ( 2nd ` y ) = d )
30 29 breq2d 
 |-  ( y = <. c , d >. -> ( b S ( 2nd ` y ) <-> b S d ) )
31 29 eqeq2d 
 |-  ( y = <. c , d >. -> ( b = ( 2nd ` y ) <-> b = d ) )
32 30 31 orbi12d 
 |-  ( y = <. c , d >. -> ( ( b S ( 2nd ` y ) \/ b = ( 2nd ` y ) ) <-> ( b S d \/ b = d ) ) )
33 neeq2 
 |-  ( y = <. c , d >. -> ( <. a , b >. =/= y <-> <. a , b >. =/= <. c , d >. ) )
34 7 8 opthne 
 |-  ( <. a , b >. =/= <. c , d >. <-> ( a =/= c \/ b =/= d ) )
35 33 34 bitrdi 
 |-  ( y = <. c , d >. -> ( <. a , b >. =/= y <-> ( a =/= c \/ b =/= d ) ) )
36 28 32 35 3anbi123d 
 |-  ( y = <. c , d >. -> ( ( ( a R ( 1st ` y ) \/ a = ( 1st ` y ) ) /\ ( b S ( 2nd ` y ) \/ b = ( 2nd ` y ) ) /\ <. a , b >. =/= y ) <-> ( ( a R c \/ a = c ) /\ ( b S d \/ b = d ) /\ ( a =/= c \/ b =/= d ) ) ) )
37 22 36 3anbi23d 
 |-  ( 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 ) \/ b = ( 2nd ` y ) ) /\ <. a , b >. =/= y ) ) <-> ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) /\ ( ( a R c \/ a = c ) /\ ( b S d \/ b = d ) /\ ( a =/= c \/ b =/= d ) ) ) ) )
38 2 3 19 37 1 brab 
 |-  ( <. a , b >. T <. c , d >. <-> ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) /\ ( ( a R c \/ a = c ) /\ ( b S d \/ b = d ) /\ ( a =/= c \/ b =/= d ) ) ) )