Metamath Proof Explorer

Theorem xpord3pred

Description: Calculate the predecsessor class for the triple order. (Contributed by Scott Fenton, 31-Jan-2025)

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 oteq1 
 |-  ( a = X -> <. a , b , c >. = <. X , b , c >. )
3 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 >. ) )
4 2 3 syl 
 |-  ( a = X -> Pred ( U , ( ( A X. B ) X. C ) , <. a , b , c >. ) = Pred ( U , ( ( A X. B ) X. C ) , <. X , b , c >. ) )
5 predeq3 
 |-  ( a = X -> Pred ( R , A , a ) = Pred ( R , A , X ) )
6 sneq 
 |-  ( a = X -> { a } = { X } )
7 5 6 uneq12d 
 |-  ( a = X -> ( Pred ( R , A , a ) u. { a } ) = ( Pred ( R , A , X ) u. { X } ) )
8 7 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 } ) ) )
9 8 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 } ) ) )
10 2 sneqd 
 |-  ( a = X -> { <. a , b , c >. } = { <. X , b , c >. } )
11 9 10 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 >. } ) )
12 4 11 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 >. } ) ) )
13 oteq2 
 |-  ( b = Y -> <. X , b , c >. = <. X , Y , c >. )
14 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 >. ) )
15 13 14 syl 
 |-  ( b = Y -> Pred ( U , ( ( A X. B ) X. C ) , <. X , b , c >. ) = Pred ( U , ( ( A X. B ) X. C ) , <. X , Y , c >. ) )
16 predeq3 
 |-  ( b = Y -> Pred ( S , B , b ) = Pred ( S , B , Y ) )
17 sneq 
 |-  ( b = Y -> { b } = { Y } )
18 16 17 uneq12d 
 |-  ( b = Y -> ( Pred ( S , B , b ) u. { b } ) = ( Pred ( S , B , Y ) u. { Y } ) )
19 18 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 } ) ) )
20 19 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 } ) ) )
21 13 sneqd 
 |-  ( b = Y -> { <. X , b , c >. } = { <. X , Y , c >. } )
22 20 21 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 >. } ) )
23 15 22 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 >. } ) ) )
24 oteq3 
 |-  ( c = Z -> <. X , Y , c >. = <. X , Y , Z >. )
25 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 >. ) )
26 24 25 syl 
 |-  ( c = Z -> Pred ( U , ( ( A X. B ) X. C ) , <. X , Y , c >. ) = Pred ( U , ( ( A X. B ) X. C ) , <. X , Y , Z >. ) )
27 predeq3 
 |-  ( c = Z -> Pred ( T , C , c ) = Pred ( T , C , Z ) )
28 sneq 
 |-  ( c = Z -> { c } = { Z } )
29 27 28 uneq12d 
 |-  ( c = Z -> ( Pred ( T , C , c ) u. { c } ) = ( Pred ( T , C , Z ) u. { Z } ) )
30 29 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 } ) ) )
31 24 sneqd 
 |-  ( c = Z -> { <. X , Y , c >. } = { <. X , Y , Z >. } )
32 30 31 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 >. } ) )
33 26 32 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 >. } ) ) )
34 el2xptp 
 |-  ( q e. ( ( A X. B ) X. C ) <-> E. d e. A E. e e. B E. f e. C q = <. d , e , f >. )
35 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 ) ) ) )
36 simplrl 
 |-  ( ( ( ( a e. A /\ b e. B /\ c e. C ) /\ ( d e. A /\ e e. B ) ) /\ f e. C ) -> d e. A )
37 simplrr 
 |-  ( ( ( ( a e. A /\ b e. B /\ c e. C ) /\ ( d e. A /\ e e. B ) ) /\ f e. C ) -> e e. B )
38 simpr 
 |-  ( ( ( ( a e. A /\ b e. B /\ c e. C ) /\ ( d e. A /\ e e. B ) ) /\ f e. C ) -> f e. C )
39 36 37 38 3jca 
 |-  ( ( ( ( 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 ) )
40 simpll 
 |-  ( ( ( ( a e. A /\ b e. B /\ c e. C ) /\ ( d e. A /\ e e. B ) ) /\ f e. C ) -> ( a e. A /\ b e. B /\ c e. C ) )
41 39 40 jca 
 |-  ( ( ( ( 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 ) ) )
42 41 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 ) ) ) ) )
43 36 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 ) ) )
44 43 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 ) ) )
45 37 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 ) ) )
46 45 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 ) ) )
47 38 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 ) ) )
48 47 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 ) ) )
49 44 46 48 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 ) ) ) )
50 49 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 ) ) ) )
51 42 50 bitr3d 
 |-  ( ( ( ( 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. 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 ) ) ) )
52 35 51 bitrid 
 |-  ( ( ( ( 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. 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 ) ) ) )
53 breq1 
 |-  ( q = <. d , e , f >. -> ( q U <. a , b , c >. <-> <. d , e , f >. U <. a , b , c >. ) )
54 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 ) ) ) )
55 53 54 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 ) ) ) ) )
56 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 >. } ) ) )
57 eldifsn 
 |-  ( <. 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 >. =/= <. a , b , c >. ) )
58 otelxp 
 |-  ( <. 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. ( Pred ( R , A , a ) u. { a } ) /\ e e. ( Pred ( S , B , b ) u. { b } ) /\ f e. ( Pred ( T , C , c ) u. { c } ) ) )
59 elun 
 |-  ( d e. ( Pred ( R , A , a ) u. { a } ) <-> ( d e. Pred ( R , A , a ) \/ d e. { a } ) )
60 vex 
 |-  d e. _V
61 60 elpred 
 |-  ( a e. _V -> ( d e. Pred ( R , A , a ) <-> ( d e. A /\ d R a ) ) )
62 61 elv 
 |-  ( d e. Pred ( R , A , a ) <-> ( d e. A /\ d R a ) )
63 velsn 
 |-  ( d e. { a } <-> d = a )
64 62 63 orbi12i 
 |-  ( ( d e. Pred ( R , A , a ) \/ d e. { a } ) <-> ( ( d e. A /\ d R a ) \/ d = a ) )
65 59 64 bitri 
 |-  ( d e. ( Pred ( R , A , a ) u. { a } ) <-> ( ( d e. A /\ d R a ) \/ d = a ) )
66 elun 
 |-  ( e e. ( Pred ( S , B , b ) u. { b } ) <-> ( e e. Pred ( S , B , b ) \/ e e. { b } ) )
67 vex 
 |-  e e. _V
68 67 elpred 
 |-  ( b e. _V -> ( e e. Pred ( S , B , b ) <-> ( e e. B /\ e S b ) ) )
69 68 elv 
 |-  ( e e. Pred ( S , B , b ) <-> ( e e. B /\ e S b ) )
70 velsn 
 |-  ( e e. { b } <-> e = b )
71 69 70 orbi12i 
 |-  ( ( e e. Pred ( S , B , b ) \/ e e. { b } ) <-> ( ( e e. B /\ e S b ) \/ e = b ) )
72 66 71 bitri 
 |-  ( e e. ( Pred ( S , B , b ) u. { b } ) <-> ( ( e e. B /\ e S b ) \/ e = b ) )
73 elun 
 |-  ( f e. ( Pred ( T , C , c ) u. { c } ) <-> ( f e. Pred ( T , C , c ) \/ f e. { c } ) )
74 vex 
 |-  f e. _V
75 74 elpred 
 |-  ( c e. _V -> ( f e. Pred ( T , C , c ) <-> ( f e. C /\ f T c ) ) )
76 75 elv 
 |-  ( f e. Pred ( T , C , c ) <-> ( f e. C /\ f T c ) )
77 velsn 
 |-  ( f e. { c } <-> f = c )
78 76 77 orbi12i 
 |-  ( ( f e. Pred ( T , C , c ) \/ f e. { c } ) <-> ( ( f e. C /\ f T c ) \/ f = c ) )
79 73 78 bitri 
 |-  ( f e. ( Pred ( T , C , c ) u. { c } ) <-> ( ( f e. C /\ f T c ) \/ f = c ) )
80 65 72 79 3anbi123i 
 |-  ( ( d e. ( Pred ( R , A , a ) u. { a } ) /\ e e. ( 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 ) ) )
81 58 80 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 ) ) )
82 60 67 74 otthne 
 |-  ( <. d , e , f >. =/= <. a , b , c >. <-> ( d =/= a \/ e =/= b \/ f =/= c ) )
83 81 82 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 >. =/= <. 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 ) ) )
84 57 83 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 ) ) )
85 56 84 bitrdi 
 |-  ( 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. 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 ) ) ) )
86 55 85 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. 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 ) ) ) ) )
87 52 86 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 >. } ) ) ) )
88 87 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 >. } ) ) ) )
89 88 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 >. } ) ) ) )
90 34 89 biimtrid 
 |-  ( ( 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 >. } ) ) ) )
91 90 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 >. } ) ) ) )
92 otex 
 |-  <. a , b , c >. e. _V
93 vex 
 |-  q e. _V
94 93 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 >. ) ) )
95 92 94 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 >. ) )
96 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 >. } ) ) )
97 91 95 96 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 >. } ) ) ) )
98 97 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 >. } ) ) )
99 predss 
 |-  Pred ( R , A , a ) C_ A
100 99 a1i 
 |-  ( a e. A -> Pred ( R , A , a ) C_ A )
101 snssi 
 |-  ( a e. A -> { a } C_ A )
102 100 101 unssd 
 |-  ( a e. A -> ( Pred ( R , A , a ) u. { a } ) C_ A )
103 102 3ad2ant1 
 |-  ( ( a e. A /\ b e. B /\ c e. C ) -> ( Pred ( R , A , a ) u. { a } ) C_ A )
104 predss 
 |-  Pred ( S , B , b ) C_ B
105 104 a1i 
 |-  ( b e. B -> Pred ( S , B , b ) C_ B )
106 snssi 
 |-  ( b e. B -> { b } C_ B )
107 105 106 unssd 
 |-  ( b e. B -> ( Pred ( S , B , b ) u. { b } ) C_ B )
108 107 3ad2ant2 
 |-  ( ( a e. A /\ b e. B /\ c e. C ) -> ( Pred ( S , B , b ) u. { b } ) C_ B )
109 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 ) )
110 103 108 109 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 ) )
111 predss 
 |-  Pred ( T , C , c ) C_ C
112 111 a1i 
 |-  ( c e. C -> Pred ( T , C , c ) C_ C )
113 snssi 
 |-  ( c e. C -> { c } C_ C )
114 112 113 unssd 
 |-  ( c e. C -> ( Pred ( T , C , c ) u. { c } ) C_ C )
115 114 3ad2ant3 
 |-  ( ( a e. A /\ b e. B /\ c e. C ) -> ( Pred ( T , C , c ) u. { c } ) C_ C )
116 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 ) )
117 110 115 116 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 ) )
118 117 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 ) )
119 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 >. } ) )
120 118 119 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 >. } ) )
121 98 120 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 >. } ) )
122 12 23 33 121 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 >. } ) )