Metamath Proof Explorer

Theorem xpord3lem

Description: Lemma for triple ordering. Calculate the value of the relation. (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 otex 
 |-  <. a , b , c >. e. _V
3 otex 
 |-  <. 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 2fveq3 
 |-  ( x = <. a , b , c >. -> ( 1st ` ( 1st ` x ) ) = ( 1st ` ( 1st ` <. a , b , c >. ) ) )
6 vex 
 |-  a e. _V
7 vex 
 |-  b e. _V
8 vex 
 |-  c e. _V
9 ot1stg 
 |-  ( ( a e. _V /\ b e. _V /\ c e. _V ) -> ( 1st ` ( 1st ` <. a , b , c >. ) ) = a )
10 6 7 8 9 mp3an 
 |-  ( 1st ` ( 1st ` <. a , b , c >. ) ) = a
11 5 10 eqtrdi 
 |-  ( x = <. a , b , c >. -> ( 1st ` ( 1st ` x ) ) = a )
12 11 breq1d 
 |-  ( x = <. a , b , c >. -> ( ( 1st ` ( 1st ` x ) ) R ( 1st ` ( 1st ` y ) ) <-> a R ( 1st ` ( 1st ` y ) ) ) )
13 11 eqeq1d 
 |-  ( x = <. a , b , c >. -> ( ( 1st ` ( 1st ` x ) ) = ( 1st ` ( 1st ` y ) ) <-> a = ( 1st ` ( 1st ` y ) ) ) )
14 12 13 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 ) ) ) ) )
15 2fveq3 
 |-  ( x = <. a , b , c >. -> ( 2nd ` ( 1st ` x ) ) = ( 2nd ` ( 1st ` <. a , b , c >. ) ) )
16 ot2ndg 
 |-  ( ( a e. _V /\ b e. _V /\ c e. _V ) -> ( 2nd ` ( 1st ` <. a , b , c >. ) ) = b )
17 6 7 8 16 mp3an 
 |-  ( 2nd ` ( 1st ` <. a , b , c >. ) ) = b
18 15 17 eqtrdi 
 |-  ( x = <. a , b , c >. -> ( 2nd ` ( 1st ` x ) ) = b )
19 18 breq1d 
 |-  ( x = <. a , b , c >. -> ( ( 2nd ` ( 1st ` x ) ) S ( 2nd ` ( 1st ` y ) ) <-> b S ( 2nd ` ( 1st ` y ) ) ) )
20 18 eqeq1d 
 |-  ( x = <. a , b , c >. -> ( ( 2nd ` ( 1st ` x ) ) = ( 2nd ` ( 1st ` y ) ) <-> b = ( 2nd ` ( 1st ` y ) ) ) )
21 19 20 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 ) ) ) ) )
22 fveq2 
 |-  ( x = <. a , b , c >. -> ( 2nd ` x ) = ( 2nd ` <. a , b , c >. ) )
23 ot3rdg 
 |-  ( c e. _V -> ( 2nd ` <. a , b , c >. ) = c )
24 23 elv 
 |-  ( 2nd ` <. a , b , c >. ) = c
25 22 24 eqtrdi 
 |-  ( x = <. a , b , c >. -> ( 2nd ` x ) = c )
26 25 breq1d 
 |-  ( x = <. a , b , c >. -> ( ( 2nd ` x ) T ( 2nd ` y ) <-> c T ( 2nd ` y ) ) )
27 25 eqeq1d 
 |-  ( x = <. a , b , c >. -> ( ( 2nd ` x ) = ( 2nd ` y ) <-> c = ( 2nd ` y ) ) )
28 26 27 orbi12d 
 |-  ( x = <. a , b , c >. -> ( ( ( 2nd ` x ) T ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) <-> ( c T ( 2nd ` y ) \/ c = ( 2nd ` y ) ) ) )
29 14 21 28 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 ) ) ) ) )
30 neeq1 
 |-  ( x = <. a , b , c >. -> ( x =/= y <-> <. a , b , c >. =/= y ) )
31 29 30 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 ) ) )
32 4 31 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 ) ) ) )
33 eleq1 
 |-  ( y = <. d , e , f >. -> ( y e. ( ( A X. B ) X. C ) <-> <. d , e , f >. e. ( ( A X. B ) X. C ) ) )
34 2fveq3 
 |-  ( y = <. d , e , f >. -> ( 1st ` ( 1st ` y ) ) = ( 1st ` ( 1st ` <. d , e , f >. ) ) )
35 vex 
 |-  d e. _V
36 vex 
 |-  e e. _V
37 vex 
 |-  f e. _V
38 ot1stg 
 |-  ( ( d e. _V /\ e e. _V /\ f e. _V ) -> ( 1st ` ( 1st ` <. d , e , f >. ) ) = d )
39 35 36 37 38 mp3an 
 |-  ( 1st ` ( 1st ` <. d , e , f >. ) ) = d
40 34 39 eqtrdi 
 |-  ( y = <. d , e , f >. -> ( 1st ` ( 1st ` y ) ) = d )
41 40 breq2d 
 |-  ( y = <. d , e , f >. -> ( a R ( 1st ` ( 1st ` y ) ) <-> a R d ) )
42 40 eqeq2d 
 |-  ( y = <. d , e , f >. -> ( a = ( 1st ` ( 1st ` y ) ) <-> a = d ) )
43 41 42 orbi12d 
 |-  ( y = <. d , e , f >. -> ( ( a R ( 1st ` ( 1st ` y ) ) \/ a = ( 1st ` ( 1st ` y ) ) ) <-> ( a R d \/ a = d ) ) )
44 2fveq3 
 |-  ( y = <. d , e , f >. -> ( 2nd ` ( 1st ` y ) ) = ( 2nd ` ( 1st ` <. d , e , f >. ) ) )
45 ot2ndg 
 |-  ( ( d e. _V /\ e e. _V /\ f e. _V ) -> ( 2nd ` ( 1st ` <. d , e , f >. ) ) = e )
46 35 36 37 45 mp3an 
 |-  ( 2nd ` ( 1st ` <. d , e , f >. ) ) = e
47 44 46 eqtrdi 
 |-  ( y = <. d , e , f >. -> ( 2nd ` ( 1st ` y ) ) = e )
48 47 breq2d 
 |-  ( y = <. d , e , f >. -> ( b S ( 2nd ` ( 1st ` y ) ) <-> b S e ) )
49 47 eqeq2d 
 |-  ( y = <. d , e , f >. -> ( b = ( 2nd ` ( 1st ` y ) ) <-> b = e ) )
50 48 49 orbi12d 
 |-  ( y = <. d , e , f >. -> ( ( b S ( 2nd ` ( 1st ` y ) ) \/ b = ( 2nd ` ( 1st ` y ) ) ) <-> ( b S e \/ b = e ) ) )
51 fveq2 
 |-  ( y = <. d , e , f >. -> ( 2nd ` y ) = ( 2nd ` <. d , e , f >. ) )
52 ot3rdg 
 |-  ( f e. _V -> ( 2nd ` <. d , e , f >. ) = f )
53 52 elv 
 |-  ( 2nd ` <. d , e , f >. ) = f
54 51 53 eqtrdi 
 |-  ( y = <. d , e , f >. -> ( 2nd ` y ) = f )
55 54 breq2d 
 |-  ( y = <. d , e , f >. -> ( c T ( 2nd ` y ) <-> c T f ) )
56 54 eqeq2d 
 |-  ( y = <. d , e , f >. -> ( c = ( 2nd ` y ) <-> c = f ) )
57 55 56 orbi12d 
 |-  ( y = <. d , e , f >. -> ( ( c T ( 2nd ` y ) \/ c = ( 2nd ` y ) ) <-> ( c T f \/ c = f ) ) )
58 43 50 57 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 ) ) ) )
59 neeq2 
 |-  ( y = <. d , e , f >. -> ( <. a , b , c >. =/= y <-> <. a , b , c >. =/= <. d , e , f >. ) )
60 58 59 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 >. ) ) )
61 33 60 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 >. ) ) ) )
62 2 3 32 61 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 >. ) ) )
63 otelxp 
 |-  ( <. a , b , c >. e. ( ( A X. B ) X. C ) <-> ( a e. A /\ b e. B /\ c e. C ) )
64 otelxp 
 |-  ( <. d , e , f >. e. ( ( A X. B ) X. C ) <-> ( d e. A /\ e e. B /\ f e. C ) )
65 6 7 8 otthne 
 |-  ( <. a , b , c >. =/= <. d , e , f >. <-> ( a =/= d \/ b =/= e \/ c =/= f ) )
66 65 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 ) ) )
67 63 64 66 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 ) ) ) )
68 62 67 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 ) ) ) )