Metamath Proof Explorer

Theorem xpord3lem

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

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

Proof

Step Hyp Ref Expression
1 xpord3.1 
 |-  U = { <. x , y >. | ( x e. ( ( A X. B ) X. C ) /\ y e. ( ( A X. B ) X. C ) /\ ( ( ( ( 1st ` ( 1st ` x ) ) R ( 1st ` ( 1st ` y ) ) \/ ( 1st ` ( 1st ` x ) ) = ( 1st ` ( 1st ` y ) ) ) /\ ( ( 2nd ` ( 1st ` x ) ) S ( 2nd ` ( 1st ` y ) ) \/ ( 2nd ` ( 1st ` x ) ) = ( 2nd ` ( 1st ` y ) ) ) /\ ( ( 2nd ` x ) T ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) ) /\ x =/= y ) ) }
2 opex 
 |-  <. <. a , b >. , c >. e. _V
3 opex 
 |-  <. <. d , e >. , f >. e. _V
4 eleq1 
 |-  ( x = <. <. a , b >. , c >. -> ( x e. ( ( A X. B ) X. C ) <-> <. <. a , b >. , c >. e. ( ( A X. B ) X. C ) ) )
5 vex 
 |-  a e. _V
6 vex 
 |-  b e. _V
7 vex 
 |-  c e. _V
8 5 6 7 ot21std 
 |-  ( x = <. <. a , b >. , c >. -> ( 1st ` ( 1st ` x ) ) = a )
9 8 breq1d 
 |-  ( x = <. <. a , b >. , c >. -> ( ( 1st ` ( 1st ` x ) ) R ( 1st ` ( 1st ` y ) ) <-> a R ( 1st ` ( 1st ` y ) ) ) )
10 8 eqeq1d 
 |-  ( x = <. <. a , b >. , c >. -> ( ( 1st ` ( 1st ` x ) ) = ( 1st ` ( 1st ` y ) ) <-> a = ( 1st ` ( 1st ` y ) ) ) )
11 9 10 orbi12d 
 |-  ( x = <. <. a , b >. , c >. -> ( ( ( 1st ` ( 1st ` x ) ) R ( 1st ` ( 1st ` y ) ) \/ ( 1st ` ( 1st ` x ) ) = ( 1st ` ( 1st ` y ) ) ) <-> ( a R ( 1st ` ( 1st ` y ) ) \/ a = ( 1st ` ( 1st ` y ) ) ) ) )
12 5 6 7 ot22ndd 
 |-  ( x = <. <. a , b >. , c >. -> ( 2nd ` ( 1st ` x ) ) = b )
13 12 breq1d 
 |-  ( x = <. <. a , b >. , c >. -> ( ( 2nd ` ( 1st ` x ) ) S ( 2nd ` ( 1st ` y ) ) <-> b S ( 2nd ` ( 1st ` y ) ) ) )
14 12 eqeq1d 
 |-  ( x = <. <. a , b >. , c >. -> ( ( 2nd ` ( 1st ` x ) ) = ( 2nd ` ( 1st ` y ) ) <-> b = ( 2nd ` ( 1st ` y ) ) ) )
15 13 14 orbi12d 
 |-  ( x = <. <. a , b >. , c >. -> ( ( ( 2nd ` ( 1st ` x ) ) S ( 2nd ` ( 1st ` y ) ) \/ ( 2nd ` ( 1st ` x ) ) = ( 2nd ` ( 1st ` y ) ) ) <-> ( b S ( 2nd ` ( 1st ` y ) ) \/ b = ( 2nd ` ( 1st ` y ) ) ) ) )
16 opex 
 |-  <. a , b >. e. _V
17 16 7 op2ndd 
 |-  ( x = <. <. a , b >. , c >. -> ( 2nd ` x ) = c )
18 17 breq1d 
 |-  ( x = <. <. a , b >. , c >. -> ( ( 2nd ` x ) T ( 2nd ` y ) <-> c T ( 2nd ` y ) ) )
19 17 eqeq1d 
 |-  ( x = <. <. a , b >. , c >. -> ( ( 2nd ` x ) = ( 2nd ` y ) <-> c = ( 2nd ` y ) ) )
20 18 19 orbi12d 
 |-  ( x = <. <. a , b >. , c >. -> ( ( ( 2nd ` x ) T ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) <-> ( c T ( 2nd ` y ) \/ c = ( 2nd ` y ) ) ) )
21 11 15 20 3anbi123d 
 |-  ( x = <. <. a , b >. , c >. -> ( ( ( ( 1st ` ( 1st ` x ) ) R ( 1st ` ( 1st ` y ) ) \/ ( 1st ` ( 1st ` x ) ) = ( 1st ` ( 1st ` y ) ) ) /\ ( ( 2nd ` ( 1st ` x ) ) S ( 2nd ` ( 1st ` y ) ) \/ ( 2nd ` ( 1st ` x ) ) = ( 2nd ` ( 1st ` y ) ) ) /\ ( ( 2nd ` x ) T ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) ) <-> ( ( a R ( 1st ` ( 1st ` y ) ) \/ a = ( 1st ` ( 1st ` y ) ) ) /\ ( b S ( 2nd ` ( 1st ` y ) ) \/ b = ( 2nd ` ( 1st ` y ) ) ) /\ ( c T ( 2nd ` y ) \/ c = ( 2nd ` y ) ) ) ) )
22 neeq1 
 |-  ( x = <. <. a , b >. , c >. -> ( x =/= y <-> <. <. a , b >. , c >. =/= y ) )
23 21 22 anbi12d 
 |-  ( x = <. <. a , b >. , c >. -> ( ( ( ( ( 1st ` ( 1st ` x ) ) R ( 1st ` ( 1st ` y ) ) \/ ( 1st ` ( 1st ` x ) ) = ( 1st ` ( 1st ` y ) ) ) /\ ( ( 2nd ` ( 1st ` x ) ) S ( 2nd ` ( 1st ` y ) ) \/ ( 2nd ` ( 1st ` x ) ) = ( 2nd ` ( 1st ` y ) ) ) /\ ( ( 2nd ` x ) T ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) ) /\ x =/= y ) <-> ( ( ( a R ( 1st ` ( 1st ` y ) ) \/ a = ( 1st ` ( 1st ` y ) ) ) /\ ( b S ( 2nd ` ( 1st ` y ) ) \/ b = ( 2nd ` ( 1st ` y ) ) ) /\ ( c T ( 2nd ` y ) \/ c = ( 2nd ` y ) ) ) /\ <. <. a , b >. , c >. =/= y ) ) )
24 4 23 3anbi13d 
 |-  ( x = <. <. a , b >. , c >. -> ( ( x e. ( ( A X. B ) X. C ) /\ y e. ( ( A X. B ) X. C ) /\ ( ( ( ( 1st ` ( 1st ` x ) ) R ( 1st ` ( 1st ` y ) ) \/ ( 1st ` ( 1st ` x ) ) = ( 1st ` ( 1st ` y ) ) ) /\ ( ( 2nd ` ( 1st ` x ) ) S ( 2nd ` ( 1st ` y ) ) \/ ( 2nd ` ( 1st ` x ) ) = ( 2nd ` ( 1st ` y ) ) ) /\ ( ( 2nd ` x ) T ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) ) /\ x =/= y ) ) <-> ( <. <. a , b >. , c >. e. ( ( A X. B ) X. C ) /\ y e. ( ( A X. B ) X. C ) /\ ( ( ( a R ( 1st ` ( 1st ` y ) ) \/ a = ( 1st ` ( 1st ` y ) ) ) /\ ( b S ( 2nd ` ( 1st ` y ) ) \/ b = ( 2nd ` ( 1st ` y ) ) ) /\ ( c T ( 2nd ` y ) \/ c = ( 2nd ` y ) ) ) /\ <. <. a , b >. , c >. =/= y ) ) ) )
25 eleq1 
 |-  ( y = <. <. d , e >. , f >. -> ( y e. ( ( A X. B ) X. C ) <-> <. <. d , e >. , f >. e. ( ( A X. B ) X. C ) ) )
26 vex 
 |-  d e. _V
27 vex 
 |-  e e. _V
28 vex 
 |-  f e. _V
29 26 27 28 ot21std 
 |-  ( y = <. <. d , e >. , f >. -> ( 1st ` ( 1st ` y ) ) = d )
30 29 breq2d 
 |-  ( y = <. <. d , e >. , f >. -> ( a R ( 1st ` ( 1st ` y ) ) <-> a R d ) )
31 29 eqeq2d 
 |-  ( y = <. <. d , e >. , f >. -> ( a = ( 1st ` ( 1st ` y ) ) <-> a = d ) )
32 30 31 orbi12d 
 |-  ( y = <. <. d , e >. , f >. -> ( ( a R ( 1st ` ( 1st ` y ) ) \/ a = ( 1st ` ( 1st ` y ) ) ) <-> ( a R d \/ a = d ) ) )
33 26 27 28 ot22ndd 
 |-  ( y = <. <. d , e >. , f >. -> ( 2nd ` ( 1st ` y ) ) = e )
34 33 breq2d 
 |-  ( y = <. <. d , e >. , f >. -> ( b S ( 2nd ` ( 1st ` y ) ) <-> b S e ) )
35 33 eqeq2d 
 |-  ( y = <. <. d , e >. , f >. -> ( b = ( 2nd ` ( 1st ` y ) ) <-> b = e ) )
36 34 35 orbi12d 
 |-  ( y = <. <. d , e >. , f >. -> ( ( b S ( 2nd ` ( 1st ` y ) ) \/ b = ( 2nd ` ( 1st ` y ) ) ) <-> ( b S e \/ b = e ) ) )
37 opex 
 |-  <. d , e >. e. _V
38 37 28 op2ndd 
 |-  ( y = <. <. d , e >. , f >. -> ( 2nd ` y ) = f )
39 38 breq2d 
 |-  ( y = <. <. d , e >. , f >. -> ( c T ( 2nd ` y ) <-> c T f ) )
40 38 eqeq2d 
 |-  ( y = <. <. d , e >. , f >. -> ( c = ( 2nd ` y ) <-> c = f ) )
41 39 40 orbi12d 
 |-  ( y = <. <. d , e >. , f >. -> ( ( c T ( 2nd ` y ) \/ c = ( 2nd ` y ) ) <-> ( c T f \/ c = f ) ) )
42 32 36 41 3anbi123d 
 |-  ( y = <. <. d , e >. , f >. -> ( ( ( a R ( 1st ` ( 1st ` y ) ) \/ a = ( 1st ` ( 1st ` y ) ) ) /\ ( b S ( 2nd ` ( 1st ` y ) ) \/ b = ( 2nd ` ( 1st ` y ) ) ) /\ ( c T ( 2nd ` y ) \/ c = ( 2nd ` y ) ) ) <-> ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) ) )
43 neeq2 
 |-  ( y = <. <. d , e >. , f >. -> ( <. <. a , b >. , c >. =/= y <-> <. <. a , b >. , c >. =/= <. <. d , e >. , f >. ) )
44 42 43 anbi12d 
 |-  ( y = <. <. d , e >. , f >. -> ( ( ( ( a R ( 1st ` ( 1st ` y ) ) \/ a = ( 1st ` ( 1st ` y ) ) ) /\ ( b S ( 2nd ` ( 1st ` y ) ) \/ b = ( 2nd ` ( 1st ` y ) ) ) /\ ( c T ( 2nd ` y ) \/ c = ( 2nd ` y ) ) ) /\ <. <. a , b >. , c >. =/= y ) <-> ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ <. <. a , b >. , c >. =/= <. <. d , e >. , f >. ) ) )
45 25 44 3anbi23d 
 |-  ( y = <. <. d , e >. , f >. -> ( ( <. <. a , b >. , c >. e. ( ( A X. B ) X. C ) /\ y e. ( ( A X. B ) X. C ) /\ ( ( ( a R ( 1st ` ( 1st ` y ) ) \/ a = ( 1st ` ( 1st ` y ) ) ) /\ ( b S ( 2nd ` ( 1st ` y ) ) \/ b = ( 2nd ` ( 1st ` y ) ) ) /\ ( c T ( 2nd ` y ) \/ c = ( 2nd ` y ) ) ) /\ <. <. a , b >. , c >. =/= y ) ) <-> ( <. <. a , b >. , c >. e. ( ( A X. B ) X. C ) /\ <. <. d , e >. , f >. e. ( ( A X. B ) X. C ) /\ ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ <. <. a , b >. , c >. =/= <. <. d , e >. , f >. ) ) ) )
46 2 3 24 45 1 brab 
 |-  ( <. <. a , b >. , c >. U <. <. d , e >. , f >. <-> ( <. <. a , b >. , c >. e. ( ( A X. B ) X. C ) /\ <. <. d , e >. , f >. e. ( ( A X. B ) X. C ) /\ ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ <. <. a , b >. , c >. =/= <. <. d , e >. , f >. ) ) )
47 ot2elxp 
 |-  ( <. <. a , b >. , c >. e. ( ( A X. B ) X. C ) <-> ( a e. A /\ b e. B /\ c e. C ) )
48 ot2elxp 
 |-  ( <. <. d , e >. , f >. e. ( ( A X. B ) X. C ) <-> ( d e. A /\ e e. B /\ f e. C ) )
49 5 6 7 otthne 
 |-  ( <. <. a , b >. , c >. =/= <. <. d , e >. , f >. <-> ( a =/= d \/ b =/= e \/ c =/= f ) )
50 49 anbi2i 
 |-  ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ <. <. a , b >. , c >. =/= <. <. d , e >. , f >. ) <-> ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) )
51 47 48 50 3anbi123i 
 |-  ( ( <. <. a , b >. , c >. e. ( ( A X. B ) X. C ) /\ <. <. d , e >. , f >. e. ( ( A X. B ) X. C ) /\ ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ <. <. a , b >. , c >. =/= <. <. d , e >. , f >. ) ) <-> ( ( a e. A /\ b e. B /\ c e. C ) /\ ( d e. A /\ e e. B /\ f e. C ) /\ ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) ) )
52 46 51 bitri 
 |-  ( <. <. a , b >. , c >. U <. <. d , e >. , f >. <-> ( ( a e. A /\ b e. B /\ c e. C ) /\ ( d e. A /\ e e. B /\ f e. C ) /\ ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) ) )