Metamath Proof Explorer

Theorem xpord3pred

Description: Calculate the predecsessor class for the triple order. (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 xpord3pred 
|- ( ( X e. A /\ Y e. B /\ Z e. C ) -> Pred ( U , ( ( A X. B ) X. C ) , <. <. X , Y >. , Z >. ) = ( ( ( ( Pred ( R , A , X ) u. { X } ) X. ( Pred ( S , B , Y ) u. { Y } ) ) X. ( Pred ( T , C , Z ) u. { Z } ) ) \ { <. <. X , Y >. , Z >. } ) )

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 opeq1 
 |-  ( a = X -> <. a , b >. = <. X , b >. )
3 2 opeq1d 
 |-  ( a = X -> <. <. a , b >. , c >. = <. <. X , b >. , c >. )
4 predeq3 
 |-  ( <. <. a , b >. , c >. = <. <. X , b >. , c >. -> Pred ( U , ( ( A X. B ) X. C ) , <. <. a , b >. , c >. ) = Pred ( U , ( ( A X. B ) X. C ) , <. <. X , b >. , c >. ) )
5 3 4 syl 
 |-  ( a = X -> Pred ( U , ( ( A X. B ) X. C ) , <. <. a , b >. , c >. ) = Pred ( U , ( ( A X. B ) X. C ) , <. <. X , b >. , c >. ) )
6 predeq3 
 |-  ( a = X -> Pred ( R , A , a ) = Pred ( R , A , X ) )
7 sneq 
 |-  ( a = X -> { a } = { X } )
8 6 7 uneq12d 
 |-  ( a = X -> ( Pred ( R , A , a ) u. { a } ) = ( Pred ( R , A , X ) u. { X } ) )
9 8 xpeq1d 
 |-  ( a = X -> ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) = ( ( Pred ( R , A , X ) u. { X } ) X. ( Pred ( S , B , b ) u. { b } ) ) )
10 9 xpeq1d 
 |-  ( a = X -> ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) = ( ( ( Pred ( R , A , X ) u. { X } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) )
11 3 sneqd 
 |-  ( a = X -> { <. <. a , b >. , c >. } = { <. <. X , b >. , c >. } )
12 10 11 difeq12d 
 |-  ( a = X -> ( ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. a , b >. , c >. } ) = ( ( ( ( Pred ( R , A , X ) u. { X } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. X , b >. , c >. } ) )
13 5 12 eqeq12d 
 |-  ( a = X -> ( Pred ( U , ( ( A X. B ) X. C ) , <. <. a , b >. , c >. ) = ( ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. a , b >. , c >. } ) <-> Pred ( U , ( ( A X. B ) X. C ) , <. <. X , b >. , c >. ) = ( ( ( ( Pred ( R , A , X ) u. { X } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. X , b >. , c >. } ) ) )
14 opeq2 
 |-  ( b = Y -> <. X , b >. = <. X , Y >. )
15 14 opeq1d 
 |-  ( b = Y -> <. <. X , b >. , c >. = <. <. X , Y >. , c >. )
16 predeq3 
 |-  ( <. <. X , b >. , c >. = <. <. X , Y >. , c >. -> Pred ( U , ( ( A X. B ) X. C ) , <. <. X , b >. , c >. ) = Pred ( U , ( ( A X. B ) X. C ) , <. <. X , Y >. , c >. ) )
17 15 16 syl 
 |-  ( b = Y -> Pred ( U , ( ( A X. B ) X. C ) , <. <. X , b >. , c >. ) = Pred ( U , ( ( A X. B ) X. C ) , <. <. X , Y >. , c >. ) )
18 predeq3 
 |-  ( b = Y -> Pred ( S , B , b ) = Pred ( S , B , Y ) )
19 sneq 
 |-  ( b = Y -> { b } = { Y } )
20 18 19 uneq12d 
 |-  ( b = Y -> ( Pred ( S , B , b ) u. { b } ) = ( Pred ( S , B , Y ) u. { Y } ) )
21 20 xpeq2d 
 |-  ( b = Y -> ( ( Pred ( R , A , X ) u. { X } ) X. ( Pred ( S , B , b ) u. { b } ) ) = ( ( Pred ( R , A , X ) u. { X } ) X. ( Pred ( S , B , Y ) u. { Y } ) ) )
22 21 xpeq1d 
 |-  ( b = Y -> ( ( ( Pred ( R , A , X ) u. { X } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) = ( ( ( Pred ( R , A , X ) u. { X } ) X. ( Pred ( S , B , Y ) u. { Y } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) )
23 15 sneqd 
 |-  ( b = Y -> { <. <. X , b >. , c >. } = { <. <. X , Y >. , c >. } )
24 22 23 difeq12d 
 |-  ( b = Y -> ( ( ( ( Pred ( R , A , X ) u. { X } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. X , b >. , c >. } ) = ( ( ( ( Pred ( R , A , X ) u. { X } ) X. ( Pred ( S , B , Y ) u. { Y } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. X , Y >. , c >. } ) )
25 17 24 eqeq12d 
 |-  ( b = Y -> ( Pred ( U , ( ( A X. B ) X. C ) , <. <. X , b >. , c >. ) = ( ( ( ( Pred ( R , A , X ) u. { X } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. X , b >. , c >. } ) <-> Pred ( U , ( ( A X. B ) X. C ) , <. <. X , Y >. , c >. ) = ( ( ( ( Pred ( R , A , X ) u. { X } ) X. ( Pred ( S , B , Y ) u. { Y } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. X , Y >. , c >. } ) ) )
26 opeq2 
 |-  ( c = Z -> <. <. X , Y >. , c >. = <. <. X , Y >. , Z >. )
27 predeq3 
 |-  ( <. <. X , Y >. , c >. = <. <. X , Y >. , Z >. -> Pred ( U , ( ( A X. B ) X. C ) , <. <. X , Y >. , c >. ) = Pred ( U , ( ( A X. B ) X. C ) , <. <. X , Y >. , Z >. ) )
28 26 27 syl 
 |-  ( c = Z -> Pred ( U , ( ( A X. B ) X. C ) , <. <. X , Y >. , c >. ) = Pred ( U , ( ( A X. B ) X. C ) , <. <. X , Y >. , Z >. ) )
29 predeq3 
 |-  ( c = Z -> Pred ( T , C , c ) = Pred ( T , C , Z ) )
30 sneq 
 |-  ( c = Z -> { c } = { Z } )
31 29 30 uneq12d 
 |-  ( c = Z -> ( Pred ( T , C , c ) u. { c } ) = ( Pred ( T , C , Z ) u. { Z } ) )
32 31 xpeq2d 
 |-  ( c = Z -> ( ( ( Pred ( R , A , X ) u. { X } ) X. ( Pred ( S , B , Y ) u. { Y } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) = ( ( ( Pred ( R , A , X ) u. { X } ) X. ( Pred ( S , B , Y ) u. { Y } ) ) X. ( Pred ( T , C , Z ) u. { Z } ) ) )
33 26 sneqd 
 |-  ( c = Z -> { <. <. X , Y >. , c >. } = { <. <. X , Y >. , Z >. } )
34 32 33 difeq12d 
 |-  ( c = Z -> ( ( ( ( Pred ( R , A , X ) u. { X } ) X. ( Pred ( S , B , Y ) u. { Y } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. X , Y >. , c >. } ) = ( ( ( ( Pred ( R , A , X ) u. { X } ) X. ( Pred ( S , B , Y ) u. { Y } ) ) X. ( Pred ( T , C , Z ) u. { Z } ) ) \ { <. <. X , Y >. , Z >. } ) )
35 28 34 eqeq12d 
 |-  ( c = Z -> ( Pred ( U , ( ( A X. B ) X. C ) , <. <. X , Y >. , c >. ) = ( ( ( ( Pred ( R , A , X ) u. { X } ) X. ( Pred ( S , B , Y ) u. { Y } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. X , Y >. , c >. } ) <-> Pred ( U , ( ( A X. B ) X. C ) , <. <. X , Y >. , Z >. ) = ( ( ( ( Pred ( R , A , X ) u. { X } ) X. ( Pred ( S , B , Y ) u. { Y } ) ) X. ( Pred ( T , C , Z ) u. { Z } ) ) \ { <. <. X , Y >. , Z >. } ) ) )
36 elxpxp 
 |-  ( q e. ( ( A X. B ) X. C ) <-> E. d e. A E. e e. B E. f e. C q = <. <. d , e >. , f >. )
37 df-3an 
 |-  ( ( d e. A /\ e e. B /\ f e. C ) <-> ( ( d e. A /\ e e. B ) /\ f e. C ) )
38 df-3an 
 |-  ( ( ( d e. A /\ e e. B /\ f e. C ) /\ ( a e. A /\ b e. B /\ c e. C ) /\ ( ( ( d R a \/ d = a ) /\ ( e S b \/ e = b ) /\ ( f T c \/ f = c ) ) /\ ( d =/= a \/ e =/= b \/ f =/= c ) ) ) <-> ( ( ( d e. A /\ e e. B /\ f e. C ) /\ ( a e. A /\ b e. B /\ c e. C ) ) /\ ( ( ( d R a \/ d = a ) /\ ( e S b \/ e = b ) /\ ( f T c \/ f = c ) ) /\ ( d =/= a \/ e =/= b \/ f =/= c ) ) ) )
39 eldif 
 |-  ( <. <. d , e >. , f >. e. ( ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. a , b >. , c >. } ) <-> ( <. <. d , e >. , f >. e. ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) /\ -. <. <. d , e >. , f >. e. { <. <. a , b >. , c >. } ) )
40 opelxp 
 |-  ( <. <. d , e >. , f >. e. ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) <-> ( <. d , e >. e. ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) /\ f e. ( Pred ( T , C , c ) u. { c } ) ) )
41 opelxp 
 |-  ( <. d , e >. e. ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) <-> ( d e. ( Pred ( R , A , a ) u. { a } ) /\ e e. ( Pred ( S , B , b ) u. { b } ) ) )
42 elun 
 |-  ( d e. ( Pred ( R , A , a ) u. { a } ) <-> ( d e. Pred ( R , A , a ) \/ d e. { a } ) )
43 vex 
 |-  d e. _V
44 43 elpred 
 |-  ( a e. _V -> ( d e. Pred ( R , A , a ) <-> ( d e. A /\ d R a ) ) )
45 44 elv 
 |-  ( d e. Pred ( R , A , a ) <-> ( d e. A /\ d R a ) )
46 velsn 
 |-  ( d e. { a } <-> d = a )
47 45 46 orbi12i 
 |-  ( ( d e. Pred ( R , A , a ) \/ d e. { a } ) <-> ( ( d e. A /\ d R a ) \/ d = a ) )
48 42 47 bitri 
 |-  ( d e. ( Pred ( R , A , a ) u. { a } ) <-> ( ( d e. A /\ d R a ) \/ d = a ) )
49 elun 
 |-  ( e e. ( Pred ( S , B , b ) u. { b } ) <-> ( e e. Pred ( S , B , b ) \/ e e. { b } ) )
50 vex 
 |-  e e. _V
51 50 elpred 
 |-  ( b e. _V -> ( e e. Pred ( S , B , b ) <-> ( e e. B /\ e S b ) ) )
52 51 elv 
 |-  ( e e. Pred ( S , B , b ) <-> ( e e. B /\ e S b ) )
53 velsn 
 |-  ( e e. { b } <-> e = b )
54 52 53 orbi12i 
 |-  ( ( e e. Pred ( S , B , b ) \/ e e. { b } ) <-> ( ( e e. B /\ e S b ) \/ e = b ) )
55 49 54 bitri 
 |-  ( e e. ( Pred ( S , B , b ) u. { b } ) <-> ( ( e e. B /\ e S b ) \/ e = b ) )
56 48 55 anbi12i 
 |-  ( ( d e. ( Pred ( R , A , a ) u. { a } ) /\ e e. ( Pred ( S , B , b ) u. { b } ) ) <-> ( ( ( d e. A /\ d R a ) \/ d = a ) /\ ( ( e e. B /\ e S b ) \/ e = b ) ) )
57 41 56 bitri 
 |-  ( <. d , e >. e. ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) <-> ( ( ( d e. A /\ d R a ) \/ d = a ) /\ ( ( e e. B /\ e S b ) \/ e = b ) ) )
58 elun 
 |-  ( f e. ( Pred ( T , C , c ) u. { c } ) <-> ( f e. Pred ( T , C , c ) \/ f e. { c } ) )
59 vex 
 |-  f e. _V
60 59 elpred 
 |-  ( c e. _V -> ( f e. Pred ( T , C , c ) <-> ( f e. C /\ f T c ) ) )
61 60 elv 
 |-  ( f e. Pred ( T , C , c ) <-> ( f e. C /\ f T c ) )
62 velsn 
 |-  ( f e. { c } <-> f = c )
63 61 62 orbi12i 
 |-  ( ( f e. Pred ( T , C , c ) \/ f e. { c } ) <-> ( ( f e. C /\ f T c ) \/ f = c ) )
64 58 63 bitri 
 |-  ( f e. ( Pred ( T , C , c ) u. { c } ) <-> ( ( f e. C /\ f T c ) \/ f = c ) )
65 57 64 anbi12i 
 |-  ( ( <. d , e >. e. ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) /\ f e. ( Pred ( T , C , c ) u. { c } ) ) <-> ( ( ( ( d e. A /\ d R a ) \/ d = a ) /\ ( ( e e. B /\ e S b ) \/ e = b ) ) /\ ( ( f e. C /\ f T c ) \/ f = c ) ) )
66 40 65 bitri 
 |-  ( <. <. d , e >. , f >. e. ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) <-> ( ( ( ( d e. A /\ d R a ) \/ d = a ) /\ ( ( e e. B /\ e S b ) \/ e = b ) ) /\ ( ( f e. C /\ f T c ) \/ f = c ) ) )
67 df-ne 
 |-  ( <. <. d , e >. , f >. =/= <. <. a , b >. , c >. <-> -. <. <. d , e >. , f >. = <. <. a , b >. , c >. )
68 43 50 59 otthne 
 |-  ( <. <. d , e >. , f >. =/= <. <. a , b >. , c >. <-> ( d =/= a \/ e =/= b \/ f =/= c ) )
69 67 68 bitr3i 
 |-  ( -. <. <. d , e >. , f >. = <. <. a , b >. , c >. <-> ( d =/= a \/ e =/= b \/ f =/= c ) )
70 opex 
 |-  <. <. d , e >. , f >. e. _V
71 70 elsn 
 |-  ( <. <. d , e >. , f >. e. { <. <. a , b >. , c >. } <-> <. <. d , e >. , f >. = <. <. a , b >. , c >. )
72 69 71 xchnxbir 
 |-  ( -. <. <. d , e >. , f >. e. { <. <. a , b >. , c >. } <-> ( d =/= a \/ e =/= b \/ f =/= c ) )
73 66 72 anbi12i 
 |-  ( ( <. <. d , e >. , f >. e. ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) /\ -. <. <. d , e >. , f >. e. { <. <. a , b >. , c >. } ) <-> ( ( ( ( ( d e. A /\ d R a ) \/ d = a ) /\ ( ( e e. B /\ e S b ) \/ e = b ) ) /\ ( ( f e. C /\ f T c ) \/ f = c ) ) /\ ( d =/= a \/ e =/= b \/ f =/= c ) ) )
74 39 73 bitri 
 |-  ( <. <. d , e >. , f >. e. ( ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. a , b >. , c >. } ) <-> ( ( ( ( ( d e. A /\ d R a ) \/ d = a ) /\ ( ( e e. B /\ e S b ) \/ e = b ) ) /\ ( ( f e. C /\ f T c ) \/ f = c ) ) /\ ( d =/= a \/ e =/= b \/ f =/= c ) ) )
75 simpr1 
 |-  ( ( ( a e. A /\ b e. B /\ c e. C ) /\ ( d e. A /\ e e. B /\ f e. C ) ) -> d e. A )
76 75 biantrurd 
 |-  ( ( ( a e. A /\ b e. B /\ c e. C ) /\ ( d e. A /\ e e. B /\ f e. C ) ) -> ( d R a <-> ( d e. A /\ d R a ) ) )
77 76 orbi1d 
 |-  ( ( ( a e. A /\ b e. B /\ c e. C ) /\ ( d e. A /\ e e. B /\ f e. C ) ) -> ( ( d R a \/ d = a ) <-> ( ( d e. A /\ d R a ) \/ d = a ) ) )
78 simpr2 
 |-  ( ( ( a e. A /\ b e. B /\ c e. C ) /\ ( d e. A /\ e e. B /\ f e. C ) ) -> e e. B )
79 78 biantrurd 
 |-  ( ( ( a e. A /\ b e. B /\ c e. C ) /\ ( d e. A /\ e e. B /\ f e. C ) ) -> ( e S b <-> ( e e. B /\ e S b ) ) )
80 79 orbi1d 
 |-  ( ( ( a e. A /\ b e. B /\ c e. C ) /\ ( d e. A /\ e e. B /\ f e. C ) ) -> ( ( e S b \/ e = b ) <-> ( ( e e. B /\ e S b ) \/ e = b ) ) )
81 simpr3 
 |-  ( ( ( a e. A /\ b e. B /\ c e. C ) /\ ( d e. A /\ e e. B /\ f e. C ) ) -> f e. C )
82 81 biantrurd 
 |-  ( ( ( a e. A /\ b e. B /\ c e. C ) /\ ( d e. A /\ e e. B /\ f e. C ) ) -> ( f T c <-> ( f e. C /\ f T c ) ) )
83 82 orbi1d 
 |-  ( ( ( a e. A /\ b e. B /\ c e. C ) /\ ( d e. A /\ e e. B /\ f e. C ) ) -> ( ( f T c \/ f = c ) <-> ( ( f e. C /\ f T c ) \/ f = c ) ) )
84 77 80 83 3anbi123d 
 |-  ( ( ( a e. A /\ b e. B /\ c e. C ) /\ ( d e. A /\ e e. B /\ f e. C ) ) -> ( ( ( d R a \/ d = a ) /\ ( e S b \/ e = b ) /\ ( f T c \/ f = c ) ) <-> ( ( ( d e. A /\ d R a ) \/ d = a ) /\ ( ( e e. B /\ e S b ) \/ e = b ) /\ ( ( f e. C /\ f T c ) \/ f = c ) ) ) )
85 df-3an 
 |-  ( ( ( ( d e. A /\ d R a ) \/ d = a ) /\ ( ( e e. B /\ e S b ) \/ e = b ) /\ ( ( f e. C /\ f T c ) \/ f = c ) ) <-> ( ( ( ( d e. A /\ d R a ) \/ d = a ) /\ ( ( e e. B /\ e S b ) \/ e = b ) ) /\ ( ( f e. C /\ f T c ) \/ f = c ) ) )
86 84 85 bitrdi 
 |-  ( ( ( a e. A /\ b e. B /\ c e. C ) /\ ( d e. A /\ e e. B /\ f e. C ) ) -> ( ( ( d R a \/ d = a ) /\ ( e S b \/ e = b ) /\ ( f T c \/ f = c ) ) <-> ( ( ( ( d e. A /\ d R a ) \/ d = a ) /\ ( ( e e. B /\ e S b ) \/ e = b ) ) /\ ( ( f e. C /\ f T c ) \/ f = c ) ) ) )
87 86 anbi1d 
 |-  ( ( ( a e. A /\ b e. B /\ c e. C ) /\ ( d e. A /\ e e. B /\ f e. C ) ) -> ( ( ( ( d R a \/ d = a ) /\ ( e S b \/ e = b ) /\ ( f T c \/ f = c ) ) /\ ( d =/= a \/ e =/= b \/ f =/= c ) ) <-> ( ( ( ( ( d e. A /\ d R a ) \/ d = a ) /\ ( ( e e. B /\ e S b ) \/ e = b ) ) /\ ( ( f e. C /\ f T c ) \/ f = c ) ) /\ ( d =/= a \/ e =/= b \/ f =/= c ) ) ) )
88 74 87 bitr4id 
 |-  ( ( ( a e. A /\ b e. B /\ c e. C ) /\ ( d e. A /\ e e. B /\ f e. C ) ) -> ( <. <. d , e >. , f >. e. ( ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. a , b >. , c >. } ) <-> ( ( ( d R a \/ d = a ) /\ ( e S b \/ e = b ) /\ ( f T c \/ f = c ) ) /\ ( d =/= a \/ e =/= b \/ f =/= c ) ) ) )
89 pm3.22 
 |-  ( ( ( a e. A /\ b e. B /\ c e. C ) /\ ( d e. A /\ e e. B /\ f e. C ) ) -> ( ( d e. A /\ e e. B /\ f e. C ) /\ ( a e. A /\ b e. B /\ c e. C ) ) )
90 89 biantrurd 
 |-  ( ( ( a e. A /\ b e. B /\ c e. C ) /\ ( d e. A /\ e e. B /\ f e. C ) ) -> ( ( ( ( d R a \/ d = a ) /\ ( e S b \/ e = b ) /\ ( f T c \/ f = c ) ) /\ ( d =/= a \/ e =/= b \/ f =/= c ) ) <-> ( ( ( d e. A /\ e e. B /\ f e. C ) /\ ( a e. A /\ b e. B /\ c e. C ) ) /\ ( ( ( d R a \/ d = a ) /\ ( e S b \/ e = b ) /\ ( f T c \/ f = c ) ) /\ ( d =/= a \/ e =/= b \/ f =/= c ) ) ) ) )
91 88 90 bitr2d 
 |-  ( ( ( a e. A /\ b e. B /\ c e. C ) /\ ( d e. A /\ e e. B /\ f e. C ) ) -> ( ( ( ( d e. A /\ e e. B /\ f e. C ) /\ ( a e. A /\ b e. B /\ c e. C ) ) /\ ( ( ( d R a \/ d = a ) /\ ( e S b \/ e = b ) /\ ( f T c \/ f = c ) ) /\ ( d =/= a \/ e =/= b \/ f =/= c ) ) ) <-> <. <. d , e >. , f >. e. ( ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. a , b >. , c >. } ) ) )
92 38 91 syl5bb 
 |-  ( ( ( a e. A /\ b e. B /\ c e. C ) /\ ( d e. A /\ e e. B /\ f e. C ) ) -> ( ( ( d e. A /\ e e. B /\ f e. C ) /\ ( a e. A /\ b e. B /\ c e. C ) /\ ( ( ( d R a \/ d = a ) /\ ( e S b \/ e = b ) /\ ( f T c \/ f = c ) ) /\ ( d =/= a \/ e =/= b \/ f =/= c ) ) ) <-> <. <. d , e >. , f >. e. ( ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. a , b >. , c >. } ) ) )
93 breq1 
 |-  ( q = <. <. d , e >. , f >. -> ( q U <. <. a , b >. , c >. <-> <. <. d , e >. , f >. U <. <. a , b >. , c >. ) )
94 1 xpord3lem 
 |-  ( <. <. d , e >. , f >. U <. <. a , b >. , c >. <-> ( ( d e. A /\ e e. B /\ f e. C ) /\ ( a e. A /\ b e. B /\ c e. C ) /\ ( ( ( d R a \/ d = a ) /\ ( e S b \/ e = b ) /\ ( f T c \/ f = c ) ) /\ ( d =/= a \/ e =/= b \/ f =/= c ) ) ) )
95 93 94 bitrdi 
 |-  ( q = <. <. d , e >. , f >. -> ( q U <. <. a , b >. , c >. <-> ( ( d e. A /\ e e. B /\ f e. C ) /\ ( a e. A /\ b e. B /\ c e. C ) /\ ( ( ( d R a \/ d = a ) /\ ( e S b \/ e = b ) /\ ( f T c \/ f = c ) ) /\ ( d =/= a \/ e =/= b \/ f =/= c ) ) ) ) )
96 eleq1 
 |-  ( q = <. <. d , e >. , f >. -> ( q e. ( ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. a , b >. , c >. } ) <-> <. <. d , e >. , f >. e. ( ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. a , b >. , c >. } ) ) )
97 95 96 bibi12d 
 |-  ( q = <. <. d , e >. , f >. -> ( ( q U <. <. a , b >. , c >. <-> q e. ( ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. a , b >. , c >. } ) ) <-> ( ( ( d e. A /\ e e. B /\ f e. C ) /\ ( a e. A /\ b e. B /\ c e. C ) /\ ( ( ( d R a \/ d = a ) /\ ( e S b \/ e = b ) /\ ( f T c \/ f = c ) ) /\ ( d =/= a \/ e =/= b \/ f =/= c ) ) ) <-> <. <. d , e >. , f >. e. ( ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. a , b >. , c >. } ) ) ) )
98 92 97 syl5ibrcom 
 |-  ( ( ( a e. A /\ b e. B /\ c e. C ) /\ ( d e. A /\ e e. B /\ f e. C ) ) -> ( q = <. <. d , e >. , f >. -> ( q U <. <. a , b >. , c >. <-> q e. ( ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. a , b >. , c >. } ) ) ) )
99 37 98 sylan2br 
 |-  ( ( ( a e. A /\ b e. B /\ c e. C ) /\ ( ( d e. A /\ e e. B ) /\ f e. C ) ) -> ( q = <. <. d , e >. , f >. -> ( q U <. <. a , b >. , c >. <-> q e. ( ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. a , b >. , c >. } ) ) ) )
100 99 anassrs 
 |-  ( ( ( ( a e. A /\ b e. B /\ c e. C ) /\ ( d e. A /\ e e. B ) ) /\ f e. C ) -> ( q = <. <. d , e >. , f >. -> ( q U <. <. a , b >. , c >. <-> q e. ( ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. a , b >. , c >. } ) ) ) )
101 100 rexlimdva 
 |-  ( ( ( a e. A /\ b e. B /\ c e. C ) /\ ( d e. A /\ e e. B ) ) -> ( E. f e. C q = <. <. d , e >. , f >. -> ( q U <. <. a , b >. , c >. <-> q e. ( ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. a , b >. , c >. } ) ) ) )
102 101 rexlimdvva 
 |-  ( ( a e. A /\ b e. B /\ c e. C ) -> ( E. d e. A E. e e. B E. f e. C q = <. <. d , e >. , f >. -> ( q U <. <. a , b >. , c >. <-> q e. ( ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. a , b >. , c >. } ) ) ) )
103 36 102 syl5bi 
 |-  ( ( a e. A /\ b e. B /\ c e. C ) -> ( q e. ( ( A X. B ) X. C ) -> ( q U <. <. a , b >. , c >. <-> q e. ( ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. a , b >. , c >. } ) ) ) )
104 103 pm5.32d 
 |-  ( ( a e. A /\ b e. B /\ c e. C ) -> ( ( q e. ( ( A X. B ) X. C ) /\ q U <. <. a , b >. , c >. ) <-> ( q e. ( ( A X. B ) X. C ) /\ q e. ( ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. a , b >. , c >. } ) ) ) )
105 opex 
 |-  <. <. a , b >. , c >. e. _V
106 vex 
 |-  q e. _V
107 106 elpred 
 |-  ( <. <. a , b >. , c >. e. _V -> ( q e. Pred ( U , ( ( A X. B ) X. C ) , <. <. a , b >. , c >. ) <-> ( q e. ( ( A X. B ) X. C ) /\ q U <. <. a , b >. , c >. ) ) )
108 105 107 ax-mp 
 |-  ( q e. Pred ( U , ( ( A X. B ) X. C ) , <. <. a , b >. , c >. ) <-> ( q e. ( ( A X. B ) X. C ) /\ q U <. <. a , b >. , c >. ) )
109 elin 
 |-  ( q e. ( ( ( A X. B ) X. C ) i^i ( ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. a , b >. , c >. } ) ) <-> ( q e. ( ( A X. B ) X. C ) /\ q e. ( ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. a , b >. , c >. } ) ) )
110 104 108 109 3bitr4g 
 |-  ( ( a e. A /\ b e. B /\ c e. C ) -> ( q e. Pred ( U , ( ( A X. B ) X. C ) , <. <. a , b >. , c >. ) <-> q e. ( ( ( A X. B ) X. C ) i^i ( ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. a , b >. , c >. } ) ) ) )
111 110 eqrdv 
 |-  ( ( a e. A /\ b e. B /\ c e. C ) -> Pred ( U , ( ( A X. B ) X. C ) , <. <. a , b >. , c >. ) = ( ( ( A X. B ) X. C ) i^i ( ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. a , b >. , c >. } ) ) )
112 predss 
 |-  Pred ( R , A , a ) C_ A
113 112 a1i 
 |-  ( a e. A -> Pred ( R , A , a ) C_ A )
114 snssi 
 |-  ( a e. A -> { a } C_ A )
115 113 114 unssd 
 |-  ( a e. A -> ( Pred ( R , A , a ) u. { a } ) C_ A )
116 115 3ad2ant1 
 |-  ( ( a e. A /\ b e. B /\ c e. C ) -> ( Pred ( R , A , a ) u. { a } ) C_ A )
117 predss 
 |-  Pred ( S , B , b ) C_ B
118 117 a1i 
 |-  ( b e. B -> Pred ( S , B , b ) C_ B )
119 snssi 
 |-  ( b e. B -> { b } C_ B )
120 118 119 unssd 
 |-  ( b e. B -> ( Pred ( S , B , b ) u. { b } ) C_ B )
121 120 3ad2ant2 
 |-  ( ( a e. A /\ b e. B /\ c e. C ) -> ( Pred ( S , B , b ) u. { b } ) C_ B )
122 xpss12 
 |-  ( ( ( Pred ( R , A , a ) u. { a } ) C_ A /\ ( Pred ( S , B , b ) u. { b } ) C_ B ) -> ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) C_ ( A X. B ) )
123 116 121 122 syl2anc 
 |-  ( ( a e. A /\ b e. B /\ c e. C ) -> ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) C_ ( A X. B ) )
124 predss 
 |-  Pred ( T , C , c ) C_ C
125 124 a1i 
 |-  ( c e. C -> Pred ( T , C , c ) C_ C )
126 snssi 
 |-  ( c e. C -> { c } C_ C )
127 125 126 unssd 
 |-  ( c e. C -> ( Pred ( T , C , c ) u. { c } ) C_ C )
128 127 3ad2ant3 
 |-  ( ( a e. A /\ b e. B /\ c e. C ) -> ( Pred ( T , C , c ) u. { c } ) C_ C )
129 xpss12 
 |-  ( ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) C_ ( A X. B ) /\ ( Pred ( T , C , c ) u. { c } ) C_ C ) -> ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) C_ ( ( A X. B ) X. C ) )
130 123 128 129 syl2anc 
 |-  ( ( a e. A /\ b e. B /\ c e. C ) -> ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) C_ ( ( A X. B ) X. C ) )
131 130 ssdifssd 
 |-  ( ( a e. A /\ b e. B /\ c e. C ) -> ( ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. a , b >. , c >. } ) C_ ( ( A X. B ) X. C ) )
132 sseqin2 
 |-  ( ( ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. a , b >. , c >. } ) C_ ( ( A X. B ) X. C ) <-> ( ( ( A X. B ) X. C ) i^i ( ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. a , b >. , c >. } ) ) = ( ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. a , b >. , c >. } ) )
133 131 132 sylib 
 |-  ( ( a e. A /\ b e. B /\ c e. C ) -> ( ( ( A X. B ) X. C ) i^i ( ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. a , b >. , c >. } ) ) = ( ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. a , b >. , c >. } ) )
134 111 133 eqtrd 
 |-  ( ( a e. A /\ b e. B /\ c e. C ) -> Pred ( U , ( ( A X. B ) X. C ) , <. <. a , b >. , c >. ) = ( ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. a , b >. , c >. } ) )
135 13 25 35 134 vtocl3ga 
 |-  ( ( X e. A /\ Y e. B /\ Z e. C ) -> Pred ( U , ( ( A X. B ) X. C ) , <. <. X , Y >. , Z >. ) = ( ( ( ( Pred ( R , A , X ) u. { X } ) X. ( Pred ( S , B , Y ) u. { Y } ) ) X. ( Pred ( T , C , Z ) u. { Z } ) ) \ { <. <. X , Y >. , Z >. } ) )