Metamath Proof Explorer

Theorem xpord3ind

Description: Induction over the triple cross product ordering. Note that the substitutions cover all possible cases of membership in the predecessor class. (Contributed by Scott Fenton, 4-Sep-2024)

Ref Expression
Hypotheses 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 ) ) }
xpord3ind.1 
|- R Fr A
xpord3ind.2 
|- R Po A
xpord3ind.3 
|- R Se A
xpord3ind.4 
|- S Fr B
xpord3ind.5 
|- S Po B
xpord3ind.6 
|- S Se B
xpord3ind.7 
|- T Fr C
xpord3ind.8 
|- T Po C
xpord3ind.9 
|- T Se C
xpord3ind.10 
|- ( a = d -> ( ph <-> ps ) )
xpord3ind.11 
|- ( b = e -> ( ps <-> ch ) )
xpord3ind.12 
|- ( c = f -> ( ch <-> th ) )
xpord3ind.13 
|- ( a = d -> ( ta <-> th ) )
xpord3ind.14 
|- ( b = e -> ( et <-> ta ) )
xpord3ind.15 
|- ( b = e -> ( ze <-> th ) )
xpord3ind.16 
|- ( c = f -> ( si <-> ta ) )
xpord3ind.17 
|- ( a = X -> ( ph <-> rh ) )
xpord3ind.18 
|- ( b = Y -> ( rh <-> mu ) )
xpord3ind.19 
|- ( c = Z -> ( mu <-> la ) )
xpord3ind.i 
|- ( ( a e. A /\ b e. B /\ c e. C ) -> ( ( ( A. d e. Pred ( R , A , a ) A. e e. Pred ( S , B , b ) A. f e. Pred ( T , C , c ) th /\ A. d e. Pred ( R , A , a ) A. e e. Pred ( S , B , b ) ch /\ A. d e. Pred ( R , A , a ) A. f e. Pred ( T , C , c ) ze ) /\ ( A. d e. Pred ( R , A , a ) ps /\ A. e e. Pred ( S , B , b ) A. f e. Pred ( T , C , c ) ta /\ A. e e. Pred ( S , B , b ) si ) /\ A. f e. Pred ( T , C , c ) et ) -> ph ) )
Assertion xpord3ind 
|- ( ( X e. A /\ Y e. B /\ Z e. C ) -> la )

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 xpord3ind.1 
 |-  R Fr A
3 xpord3ind.2 
 |-  R Po A
4 xpord3ind.3 
 |-  R Se A
5 xpord3ind.4 
 |-  S Fr B
6 xpord3ind.5 
 |-  S Po B
7 xpord3ind.6 
 |-  S Se B
8 xpord3ind.7 
 |-  T Fr C
9 xpord3ind.8 
 |-  T Po C
10 xpord3ind.9 
 |-  T Se C
11 xpord3ind.10 
 |-  ( a = d -> ( ph <-> ps ) )
12 xpord3ind.11 
 |-  ( b = e -> ( ps <-> ch ) )
13 xpord3ind.12 
 |-  ( c = f -> ( ch <-> th ) )
14 xpord3ind.13 
 |-  ( a = d -> ( ta <-> th ) )
15 xpord3ind.14 
 |-  ( b = e -> ( et <-> ta ) )
16 xpord3ind.15 
 |-  ( b = e -> ( ze <-> th ) )
17 xpord3ind.16 
 |-  ( c = f -> ( si <-> ta ) )
18 xpord3ind.17 
 |-  ( a = X -> ( ph <-> rh ) )
19 xpord3ind.18 
 |-  ( b = Y -> ( rh <-> mu ) )
20 xpord3ind.19 
 |-  ( c = Z -> ( mu <-> la ) )
21 xpord3ind.i 
 |-  ( ( a e. A /\ b e. B /\ c e. C ) -> ( ( ( A. d e. Pred ( R , A , a ) A. e e. Pred ( S , B , b ) A. f e. Pred ( T , C , c ) th /\ A. d e. Pred ( R , A , a ) A. e e. Pred ( S , B , b ) ch /\ A. d e. Pred ( R , A , a ) A. f e. Pred ( T , C , c ) ze ) /\ ( A. d e. Pred ( R , A , a ) ps /\ A. e e. Pred ( S , B , b ) A. f e. Pred ( T , C , c ) ta /\ A. e e. Pred ( S , B , b ) si ) /\ A. f e. Pred ( T , C , c ) et ) -> ph ) )
22 2 a1i 
 |-  ( T. -> R Fr A )
23 5 a1i 
 |-  ( T. -> S Fr B )
24 8 a1i 
 |-  ( T. -> T Fr C )
25 1 22 23 24 frxp3 
 |-  ( T. -> U Fr ( ( A X. B ) X. C ) )
26 25 mptru 
 |-  U Fr ( ( A X. B ) X. C )
27 3 a1i 
 |-  ( T. -> R Po A )
28 6 a1i 
 |-  ( T. -> S Po B )
29 9 a1i 
 |-  ( T. -> T Po C )
30 1 27 28 29 poxp3 
 |-  ( T. -> U Po ( ( A X. B ) X. C ) )
31 30 mptru 
 |-  U Po ( ( A X. B ) X. C )
32 4 a1i 
 |-  ( T. -> R Se A )
33 7 a1i 
 |-  ( T. -> S Se B )
34 10 a1i 
 |-  ( T. -> T Se C )
35 1 32 33 34 sexp3 
 |-  ( T. -> U Se ( ( A X. B ) X. C ) )
36 35 mptru 
 |-  U Se ( ( A X. B ) X. C )
37 26 31 36 3pm3.2i 
 |-  ( U Fr ( ( A X. B ) X. C ) /\ U Po ( ( A X. B ) X. C ) /\ U Se ( ( A X. B ) X. C ) )
38 1 xpord3pred 
 |-  ( ( 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 >. } ) )
39 38 eleq2d 
 |-  ( ( a e. A /\ b e. B /\ c e. C ) -> ( <. <. d , e >. , f >. e. Pred ( U , ( ( A X. B ) X. 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 >. } ) ) )
40 39 imbi1d 
 |-  ( ( a e. A /\ b e. B /\ c e. C ) -> ( ( <. <. d , e >. , f >. e. Pred ( U , ( ( A X. B ) X. C ) , <. <. a , b >. , c >. ) -> th ) <-> ( <. <. 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 >. } ) -> th ) ) )
41 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 >. ) )
42 ot2elxp 
 |-  ( <. <. 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 } ) ) )
43 vex 
 |-  d e. _V
44 vex 
 |-  e e. _V
45 vex 
 |-  f e. _V
46 43 44 45 otthne 
 |-  ( <. <. d , e >. , f >. =/= <. <. a , b >. , c >. <-> ( d =/= a \/ e =/= b \/ f =/= c ) )
47 42 46 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. ( Pred ( R , A , a ) u. { a } ) /\ e e. ( Pred ( S , B , b ) u. { b } ) /\ f e. ( Pred ( T , C , c ) u. { c } ) ) /\ ( d =/= a \/ e =/= b \/ f =/= c ) ) )
48 41 47 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. ( Pred ( R , A , a ) u. { a } ) /\ e e. ( Pred ( S , B , b ) u. { b } ) /\ f e. ( Pred ( T , C , c ) u. { c } ) ) /\ ( d =/= a \/ e =/= b \/ f =/= c ) ) )
49 48 imbi1i 
 |-  ( ( <. <. 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 >. } ) -> th ) <-> ( ( ( 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 =/= a \/ e =/= b \/ f =/= c ) ) -> th ) )
50 impexp 
 |-  ( ( ( ( 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 =/= a \/ e =/= b \/ f =/= c ) ) -> th ) <-> ( ( 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 =/= a \/ e =/= b \/ f =/= c ) -> th ) ) )
51 49 50 bitr2i 
 |-  ( ( ( 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 =/= a \/ e =/= b \/ f =/= c ) -> th ) ) <-> ( <. <. 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 >. } ) -> th ) )
52 40 51 bitr4di 
 |-  ( ( a e. A /\ b e. B /\ c e. C ) -> ( ( <. <. d , e >. , f >. e. Pred ( U , ( ( A X. B ) X. C ) , <. <. a , b >. , c >. ) -> th ) <-> ( ( 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 =/= a \/ e =/= b \/ f =/= c ) -> th ) ) ) )
53 52 albidv 
 |-  ( ( a e. A /\ b e. B /\ c e. C ) -> ( A. f ( <. <. d , e >. , f >. e. Pred ( U , ( ( A X. B ) X. C ) , <. <. a , b >. , c >. ) -> th ) <-> A. f ( ( 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 =/= a \/ e =/= b \/ f =/= c ) -> th ) ) ) )
54 53 2albidv 
 |-  ( ( a e. A /\ b e. B /\ c e. C ) -> ( A. d A. e A. f ( <. <. d , e >. , f >. e. Pred ( U , ( ( A X. B ) X. C ) , <. <. a , b >. , c >. ) -> th ) <-> A. d A. e A. f ( ( 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 =/= a \/ e =/= b \/ f =/= c ) -> th ) ) ) )
55 r3al 
 |-  ( A. d e. ( Pred ( R , A , a ) u. { a } ) A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) <-> A. d A. e A. f ( ( 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 =/= a \/ e =/= b \/ f =/= c ) -> th ) ) )
56 54 55 bitr4di 
 |-  ( ( a e. A /\ b e. B /\ c e. C ) -> ( A. d A. e A. f ( <. <. d , e >. , f >. e. Pred ( U , ( ( A X. B ) X. C ) , <. <. a , b >. , c >. ) -> th ) <-> A. d e. ( Pred ( R , A , a ) u. { a } ) A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) ) )
57 ssun1 
 |-  Pred ( R , A , a ) C_ ( Pred ( R , A , a ) u. { a } )
58 ssralv 
 |-  ( Pred ( R , A , a ) C_ ( Pred ( R , A , a ) u. { a } ) -> ( A. d e. ( Pred ( R , A , a ) u. { a } ) A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. d e. Pred ( R , A , a ) A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) ) )
59 57 58 ax-mp 
 |-  ( A. d e. ( Pred ( R , A , a ) u. { a } ) A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. d e. Pred ( R , A , a ) A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
60 ssun1 
 |-  Pred ( S , B , b ) C_ ( Pred ( S , B , b ) u. { b } )
61 ssralv 
 |-  ( Pred ( S , B , b ) C_ ( Pred ( S , B , b ) u. { b } ) -> ( A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. e e. Pred ( S , B , b ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) ) )
62 60 61 ax-mp 
 |-  ( A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. e e. Pred ( S , B , b ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
63 ssun1 
 |-  Pred ( T , C , c ) C_ ( Pred ( T , C , c ) u. { c } )
64 ssralv 
 |-  ( Pred ( T , C , c ) C_ ( Pred ( T , C , c ) u. { c } ) -> ( A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. f e. Pred ( T , C , c ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) ) )
65 63 64 ax-mp 
 |-  ( A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. f e. Pred ( T , C , c ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
66 65 ralimi 
 |-  ( A. e e. Pred ( S , B , b ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. e e. Pred ( S , B , b ) A. f e. Pred ( T , C , c ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
67 62 66 syl 
 |-  ( A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. e e. Pred ( S , B , b ) A. f e. Pred ( T , C , c ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
68 67 ralimi 
 |-  ( A. d e. Pred ( R , A , a ) A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. d e. Pred ( R , A , a ) A. e e. Pred ( S , B , b ) A. f e. Pred ( T , C , c ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
69 predpoirr 
 |-  ( T Po C -> -. c e. Pred ( T , C , c ) )
70 9 69 ax-mp 
 |-  -. c e. Pred ( T , C , c )
71 eleq1w 
 |-  ( f = c -> ( f e. Pred ( T , C , c ) <-> c e. Pred ( T , C , c ) ) )
72 70 71 mtbiri 
 |-  ( f = c -> -. f e. Pred ( T , C , c ) )
73 72 necon2ai 
 |-  ( f e. Pred ( T , C , c ) -> f =/= c )
74 73 3mix3d 
 |-  ( f e. Pred ( T , C , c ) -> ( d =/= a \/ e =/= b \/ f =/= c ) )
75 pm2.27 
 |-  ( ( d =/= a \/ e =/= b \/ f =/= c ) -> ( ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> th ) )
76 74 75 syl 
 |-  ( f e. Pred ( T , C , c ) -> ( ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> th ) )
77 76 ralimia 
 |-  ( A. f e. Pred ( T , C , c ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. f e. Pred ( T , C , c ) th )
78 77 2ralimi 
 |-  ( A. d e. Pred ( R , A , a ) A. e e. Pred ( S , B , b ) A. f e. Pred ( T , C , c ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. d e. Pred ( R , A , a ) A. e e. Pred ( S , B , b ) A. f e. Pred ( T , C , c ) th )
79 59 68 78 3syl 
 |-  ( A. d e. ( Pred ( R , A , a ) u. { a } ) A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. d e. Pred ( R , A , a ) A. e e. Pred ( S , B , b ) A. f e. Pred ( T , C , c ) th )
80 ssun2 
 |-  { c } C_ ( Pred ( T , C , c ) u. { c } )
81 ssralv 
 |-  ( { c } C_ ( Pred ( T , C , c ) u. { c } ) -> ( A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. f e. { c } ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) ) )
82 80 81 ax-mp 
 |-  ( A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. f e. { c } ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
83 82 ralimi 
 |-  ( A. e e. Pred ( S , B , b ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. e e. Pred ( S , B , b ) A. f e. { c } ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
84 62 83 syl 
 |-  ( A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. e e. Pred ( S , B , b ) A. f e. { c } ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
85 84 ralimi 
 |-  ( A. d e. Pred ( R , A , a ) A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. d e. Pred ( R , A , a ) A. e e. Pred ( S , B , b ) A. f e. { c } ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
86 59 85 syl 
 |-  ( A. d e. ( Pred ( R , A , a ) u. { a } ) A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. d e. Pred ( R , A , a ) A. e e. Pred ( S , B , b ) A. f e. { c } ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
87 vex 
 |-  c e. _V
88 biidd 
 |-  ( f = c -> ( d =/= a <-> d =/= a ) )
89 biidd 
 |-  ( f = c -> ( e =/= b <-> e =/= b ) )
90 neeq1 
 |-  ( f = c -> ( f =/= c <-> c =/= c ) )
91 88 89 90 3orbi123d 
 |-  ( f = c -> ( ( d =/= a \/ e =/= b \/ f =/= c ) <-> ( d =/= a \/ e =/= b \/ c =/= c ) ) )
92 13 bicomd 
 |-  ( c = f -> ( th <-> ch ) )
93 92 equcoms 
 |-  ( f = c -> ( th <-> ch ) )
94 91 93 imbi12d 
 |-  ( f = c -> ( ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) <-> ( ( d =/= a \/ e =/= b \/ c =/= c ) -> ch ) ) )
95 87 94 ralsn 
 |-  ( A. f e. { c } ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) <-> ( ( d =/= a \/ e =/= b \/ c =/= c ) -> ch ) )
96 95 2ralbii 
 |-  ( A. d e. Pred ( R , A , a ) A. e e. Pred ( S , B , b ) A. f e. { c } ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) <-> A. d e. Pred ( R , A , a ) A. e e. Pred ( S , B , b ) ( ( d =/= a \/ e =/= b \/ c =/= c ) -> ch ) )
97 86 96 sylib 
 |-  ( A. d e. ( Pred ( R , A , a ) u. { a } ) A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. d e. Pred ( R , A , a ) A. e e. Pred ( S , B , b ) ( ( d =/= a \/ e =/= b \/ c =/= c ) -> ch ) )
98 predpoirr 
 |-  ( S Po B -> -. b e. Pred ( S , B , b ) )
99 6 98 ax-mp 
 |-  -. b e. Pred ( S , B , b )
100 eleq1w 
 |-  ( e = b -> ( e e. Pred ( S , B , b ) <-> b e. Pred ( S , B , b ) ) )
101 99 100 mtbiri 
 |-  ( e = b -> -. e e. Pred ( S , B , b ) )
102 101 necon2ai 
 |-  ( e e. Pred ( S , B , b ) -> e =/= b )
103 102 3mix2d 
 |-  ( e e. Pred ( S , B , b ) -> ( d =/= a \/ e =/= b \/ c =/= c ) )
104 pm2.27 
 |-  ( ( d =/= a \/ e =/= b \/ c =/= c ) -> ( ( ( d =/= a \/ e =/= b \/ c =/= c ) -> ch ) -> ch ) )
105 103 104 syl 
 |-  ( e e. Pred ( S , B , b ) -> ( ( ( d =/= a \/ e =/= b \/ c =/= c ) -> ch ) -> ch ) )
106 105 ralimia 
 |-  ( A. e e. Pred ( S , B , b ) ( ( d =/= a \/ e =/= b \/ c =/= c ) -> ch ) -> A. e e. Pred ( S , B , b ) ch )
107 106 ralimi 
 |-  ( A. d e. Pred ( R , A , a ) A. e e. Pred ( S , B , b ) ( ( d =/= a \/ e =/= b \/ c =/= c ) -> ch ) -> A. d e. Pred ( R , A , a ) A. e e. Pred ( S , B , b ) ch )
108 97 107 syl 
 |-  ( A. d e. ( Pred ( R , A , a ) u. { a } ) A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. d e. Pred ( R , A , a ) A. e e. Pred ( S , B , b ) ch )
109 ssun2 
 |-  { b } C_ ( Pred ( S , B , b ) u. { b } )
110 ssralv 
 |-  ( { b } C_ ( Pred ( S , B , b ) u. { b } ) -> ( A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. e e. { b } A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) ) )
111 109 110 ax-mp 
 |-  ( A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. e e. { b } A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
112 65 ralimi 
 |-  ( A. e e. { b } A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. e e. { b } A. f e. Pred ( T , C , c ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
113 111 112 syl 
 |-  ( A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. e e. { b } A. f e. Pred ( T , C , c ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
114 113 ralimi 
 |-  ( A. d e. Pred ( R , A , a ) A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. d e. Pred ( R , A , a ) A. e e. { b } A. f e. Pred ( T , C , c ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
115 59 114 syl 
 |-  ( A. d e. ( Pred ( R , A , a ) u. { a } ) A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. d e. Pred ( R , A , a ) A. e e. { b } A. f e. Pred ( T , C , c ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
116 vex 
 |-  b e. _V
117 biidd 
 |-  ( e = b -> ( d =/= a <-> d =/= a ) )
118 neeq1 
 |-  ( e = b -> ( e =/= b <-> b =/= b ) )
119 biidd 
 |-  ( e = b -> ( f =/= c <-> f =/= c ) )
120 117 118 119 3orbi123d 
 |-  ( e = b -> ( ( d =/= a \/ e =/= b \/ f =/= c ) <-> ( d =/= a \/ b =/= b \/ f =/= c ) ) )
121 equcom 
 |-  ( b = e <-> e = b )
122 bicom 
 |-  ( ( ze <-> th ) <-> ( th <-> ze ) )
123 16 121 122 3imtr3i 
 |-  ( e = b -> ( th <-> ze ) )
124 120 123 imbi12d 
 |-  ( e = b -> ( ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) <-> ( ( d =/= a \/ b =/= b \/ f =/= c ) -> ze ) ) )
125 124 ralbidv 
 |-  ( e = b -> ( A. f e. Pred ( T , C , c ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) <-> A. f e. Pred ( T , C , c ) ( ( d =/= a \/ b =/= b \/ f =/= c ) -> ze ) ) )
126 116 125 ralsn 
 |-  ( A. e e. { b } A. f e. Pred ( T , C , c ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) <-> A. f e. Pred ( T , C , c ) ( ( d =/= a \/ b =/= b \/ f =/= c ) -> ze ) )
127 126 ralbii 
 |-  ( A. d e. Pred ( R , A , a ) A. e e. { b } A. f e. Pred ( T , C , c ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) <-> A. d e. Pred ( R , A , a ) A. f e. Pred ( T , C , c ) ( ( d =/= a \/ b =/= b \/ f =/= c ) -> ze ) )
128 115 127 sylib 
 |-  ( A. d e. ( Pred ( R , A , a ) u. { a } ) A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. d e. Pred ( R , A , a ) A. f e. Pred ( T , C , c ) ( ( d =/= a \/ b =/= b \/ f =/= c ) -> ze ) )
129 73 3mix3d 
 |-  ( f e. Pred ( T , C , c ) -> ( d =/= a \/ b =/= b \/ f =/= c ) )
130 pm2.27 
 |-  ( ( d =/= a \/ b =/= b \/ f =/= c ) -> ( ( ( d =/= a \/ b =/= b \/ f =/= c ) -> ze ) -> ze ) )
131 129 130 syl 
 |-  ( f e. Pred ( T , C , c ) -> ( ( ( d =/= a \/ b =/= b \/ f =/= c ) -> ze ) -> ze ) )
132 131 ralimia 
 |-  ( A. f e. Pred ( T , C , c ) ( ( d =/= a \/ b =/= b \/ f =/= c ) -> ze ) -> A. f e. Pred ( T , C , c ) ze )
133 132 ralimi 
 |-  ( A. d e. Pred ( R , A , a ) A. f e. Pred ( T , C , c ) ( ( d =/= a \/ b =/= b \/ f =/= c ) -> ze ) -> A. d e. Pred ( R , A , a ) A. f e. Pred ( T , C , c ) ze )
134 128 133 syl 
 |-  ( A. d e. ( Pred ( R , A , a ) u. { a } ) A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. d e. Pred ( R , A , a ) A. f e. Pred ( T , C , c ) ze )
135 79 108 134 3jca 
 |-  ( A. d e. ( Pred ( R , A , a ) u. { a } ) A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> ( A. d e. Pred ( R , A , a ) A. e e. Pred ( S , B , b ) A. f e. Pred ( T , C , c ) th /\ A. d e. Pred ( R , A , a ) A. e e. Pred ( S , B , b ) ch /\ A. d e. Pred ( R , A , a ) A. f e. Pred ( T , C , c ) ze ) )
136 82 ralimi 
 |-  ( A. e e. { b } A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. e e. { b } A. f e. { c } ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
137 111 136 syl 
 |-  ( A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. e e. { b } A. f e. { c } ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
138 137 ralimi 
 |-  ( A. d e. Pred ( R , A , a ) A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. d e. Pred ( R , A , a ) A. e e. { b } A. f e. { c } ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
139 59 138 syl 
 |-  ( A. d e. ( Pred ( R , A , a ) u. { a } ) A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. d e. Pred ( R , A , a ) A. e e. { b } A. f e. { c } ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
140 95 ralbii 
 |-  ( A. e e. { b } A. f e. { c } ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) <-> A. e e. { b } ( ( d =/= a \/ e =/= b \/ c =/= c ) -> ch ) )
141 biidd 
 |-  ( e = b -> ( c =/= c <-> c =/= c ) )
142 117 118 141 3orbi123d 
 |-  ( e = b -> ( ( d =/= a \/ e =/= b \/ c =/= c ) <-> ( d =/= a \/ b =/= b \/ c =/= c ) ) )
143 12 bicomd 
 |-  ( b = e -> ( ch <-> ps ) )
144 143 equcoms 
 |-  ( e = b -> ( ch <-> ps ) )
145 142 144 imbi12d 
 |-  ( e = b -> ( ( ( d =/= a \/ e =/= b \/ c =/= c ) -> ch ) <-> ( ( d =/= a \/ b =/= b \/ c =/= c ) -> ps ) ) )
146 116 145 ralsn 
 |-  ( A. e e. { b } ( ( d =/= a \/ e =/= b \/ c =/= c ) -> ch ) <-> ( ( d =/= a \/ b =/= b \/ c =/= c ) -> ps ) )
147 140 146 bitri 
 |-  ( A. e e. { b } A. f e. { c } ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) <-> ( ( d =/= a \/ b =/= b \/ c =/= c ) -> ps ) )
148 147 ralbii 
 |-  ( A. d e. Pred ( R , A , a ) A. e e. { b } A. f e. { c } ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) <-> A. d e. Pred ( R , A , a ) ( ( d =/= a \/ b =/= b \/ c =/= c ) -> ps ) )
149 139 148 sylib 
 |-  ( A. d e. ( Pred ( R , A , a ) u. { a } ) A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. d e. Pred ( R , A , a ) ( ( d =/= a \/ b =/= b \/ c =/= c ) -> ps ) )
150 predpoirr 
 |-  ( R Po A -> -. a e. Pred ( R , A , a ) )
151 3 150 ax-mp 
 |-  -. a e. Pred ( R , A , a )
152 eleq1w 
 |-  ( d = a -> ( d e. Pred ( R , A , a ) <-> a e. Pred ( R , A , a ) ) )
153 151 152 mtbiri 
 |-  ( d = a -> -. d e. Pred ( R , A , a ) )
154 153 necon2ai 
 |-  ( d e. Pred ( R , A , a ) -> d =/= a )
155 154 3mix1d 
 |-  ( d e. Pred ( R , A , a ) -> ( d =/= a \/ b =/= b \/ c =/= c ) )
156 pm2.27 
 |-  ( ( d =/= a \/ b =/= b \/ c =/= c ) -> ( ( ( d =/= a \/ b =/= b \/ c =/= c ) -> ps ) -> ps ) )
157 155 156 syl 
 |-  ( d e. Pred ( R , A , a ) -> ( ( ( d =/= a \/ b =/= b \/ c =/= c ) -> ps ) -> ps ) )
158 157 ralimia 
 |-  ( A. d e. Pred ( R , A , a ) ( ( d =/= a \/ b =/= b \/ c =/= c ) -> ps ) -> A. d e. Pred ( R , A , a ) ps )
159 149 158 syl 
 |-  ( A. d e. ( Pred ( R , A , a ) u. { a } ) A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. d e. Pred ( R , A , a ) ps )
160 ssun2 
 |-  { a } C_ ( Pred ( R , A , a ) u. { a } )
161 ssralv 
 |-  ( { a } C_ ( Pred ( R , A , a ) u. { a } ) -> ( A. d e. ( Pred ( R , A , a ) u. { a } ) A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. d e. { a } A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) ) )
162 160 161 ax-mp 
 |-  ( A. d e. ( Pred ( R , A , a ) u. { a } ) A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. d e. { a } A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
163 67 ralimi 
 |-  ( A. d e. { a } A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. d e. { a } A. e e. Pred ( S , B , b ) A. f e. Pred ( T , C , c ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
164 162 163 syl 
 |-  ( A. d e. ( Pred ( R , A , a ) u. { a } ) A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. d e. { a } A. e e. Pred ( S , B , b ) A. f e. Pred ( T , C , c ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
165 vex 
 |-  a e. _V
166 neeq1 
 |-  ( d = a -> ( d =/= a <-> a =/= a ) )
167 biidd 
 |-  ( d = a -> ( e =/= b <-> e =/= b ) )
168 biidd 
 |-  ( d = a -> ( f =/= c <-> f =/= c ) )
169 166 167 168 3orbi123d 
 |-  ( d = a -> ( ( d =/= a \/ e =/= b \/ f =/= c ) <-> ( a =/= a \/ e =/= b \/ f =/= c ) ) )
170 14 equcoms 
 |-  ( d = a -> ( ta <-> th ) )
171 170 bicomd 
 |-  ( d = a -> ( th <-> ta ) )
172 169 171 imbi12d 
 |-  ( d = a -> ( ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) <-> ( ( a =/= a \/ e =/= b \/ f =/= c ) -> ta ) ) )
173 172 2ralbidv 
 |-  ( d = a -> ( A. e e. Pred ( S , B , b ) A. f e. Pred ( T , C , c ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) <-> A. e e. Pred ( S , B , b ) A. f e. Pred ( T , C , c ) ( ( a =/= a \/ e =/= b \/ f =/= c ) -> ta ) ) )
174 165 173 ralsn 
 |-  ( A. d e. { a } A. e e. Pred ( S , B , b ) A. f e. Pred ( T , C , c ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) <-> A. e e. Pred ( S , B , b ) A. f e. Pred ( T , C , c ) ( ( a =/= a \/ e =/= b \/ f =/= c ) -> ta ) )
175 164 174 sylib 
 |-  ( A. d e. ( Pred ( R , A , a ) u. { a } ) A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. e e. Pred ( S , B , b ) A. f e. Pred ( T , C , c ) ( ( a =/= a \/ e =/= b \/ f =/= c ) -> ta ) )
176 73 3mix3d 
 |-  ( f e. Pred ( T , C , c ) -> ( a =/= a \/ e =/= b \/ f =/= c ) )
177 pm2.27 
 |-  ( ( a =/= a \/ e =/= b \/ f =/= c ) -> ( ( ( a =/= a \/ e =/= b \/ f =/= c ) -> ta ) -> ta ) )
178 176 177 syl 
 |-  ( f e. Pred ( T , C , c ) -> ( ( ( a =/= a \/ e =/= b \/ f =/= c ) -> ta ) -> ta ) )
179 178 ralimia 
 |-  ( A. f e. Pred ( T , C , c ) ( ( a =/= a \/ e =/= b \/ f =/= c ) -> ta ) -> A. f e. Pred ( T , C , c ) ta )
180 179 ralimi 
 |-  ( A. e e. Pred ( S , B , b ) A. f e. Pred ( T , C , c ) ( ( a =/= a \/ e =/= b \/ f =/= c ) -> ta ) -> A. e e. Pred ( S , B , b ) A. f e. Pred ( T , C , c ) ta )
181 175 180 syl 
 |-  ( A. d e. ( Pred ( R , A , a ) u. { a } ) A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. e e. Pred ( S , B , b ) A. f e. Pred ( T , C , c ) ta )
182 84 ralimi 
 |-  ( A. d e. { a } A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. d e. { a } A. e e. Pred ( S , B , b ) A. f e. { c } ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
183 162 182 syl 
 |-  ( A. d e. ( Pred ( R , A , a ) u. { a } ) A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. d e. { a } A. e e. Pred ( S , B , b ) A. f e. { c } ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
184 172 2ralbidv 
 |-  ( d = a -> ( A. e e. Pred ( S , B , b ) A. f e. { c } ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) <-> A. e e. Pred ( S , B , b ) A. f e. { c } ( ( a =/= a \/ e =/= b \/ f =/= c ) -> ta ) ) )
185 165 184 ralsn 
 |-  ( A. d e. { a } A. e e. Pred ( S , B , b ) A. f e. { c } ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) <-> A. e e. Pred ( S , B , b ) A. f e. { c } ( ( a =/= a \/ e =/= b \/ f =/= c ) -> ta ) )
186 biidd 
 |-  ( f = c -> ( a =/= a <-> a =/= a ) )
187 186 89 90 3orbi123d 
 |-  ( f = c -> ( ( a =/= a \/ e =/= b \/ f =/= c ) <-> ( a =/= a \/ e =/= b \/ c =/= c ) ) )
188 17 bicomd 
 |-  ( c = f -> ( ta <-> si ) )
189 188 equcoms 
 |-  ( f = c -> ( ta <-> si ) )
190 187 189 imbi12d 
 |-  ( f = c -> ( ( ( a =/= a \/ e =/= b \/ f =/= c ) -> ta ) <-> ( ( a =/= a \/ e =/= b \/ c =/= c ) -> si ) ) )
191 87 190 ralsn 
 |-  ( A. f e. { c } ( ( a =/= a \/ e =/= b \/ f =/= c ) -> ta ) <-> ( ( a =/= a \/ e =/= b \/ c =/= c ) -> si ) )
192 191 ralbii 
 |-  ( A. e e. Pred ( S , B , b ) A. f e. { c } ( ( a =/= a \/ e =/= b \/ f =/= c ) -> ta ) <-> A. e e. Pred ( S , B , b ) ( ( a =/= a \/ e =/= b \/ c =/= c ) -> si ) )
193 185 192 bitri 
 |-  ( A. d e. { a } A. e e. Pred ( S , B , b ) A. f e. { c } ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) <-> A. e e. Pred ( S , B , b ) ( ( a =/= a \/ e =/= b \/ c =/= c ) -> si ) )
194 183 193 sylib 
 |-  ( A. d e. ( Pred ( R , A , a ) u. { a } ) A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. e e. Pred ( S , B , b ) ( ( a =/= a \/ e =/= b \/ c =/= c ) -> si ) )
195 102 3mix2d 
 |-  ( e e. Pred ( S , B , b ) -> ( a =/= a \/ e =/= b \/ c =/= c ) )
196 pm2.27 
 |-  ( ( a =/= a \/ e =/= b \/ c =/= c ) -> ( ( ( a =/= a \/ e =/= b \/ c =/= c ) -> si ) -> si ) )
197 195 196 syl 
 |-  ( e e. Pred ( S , B , b ) -> ( ( ( a =/= a \/ e =/= b \/ c =/= c ) -> si ) -> si ) )
198 197 ralimia 
 |-  ( A. e e. Pred ( S , B , b ) ( ( a =/= a \/ e =/= b \/ c =/= c ) -> si ) -> A. e e. Pred ( S , B , b ) si )
199 194 198 syl 
 |-  ( A. d e. ( Pred ( R , A , a ) u. { a } ) A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. e e. Pred ( S , B , b ) si )
200 159 181 199 3jca 
 |-  ( A. d e. ( Pred ( R , A , a ) u. { a } ) A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> ( A. d e. Pred ( R , A , a ) ps /\ A. e e. Pred ( S , B , b ) A. f e. Pred ( T , C , c ) ta /\ A. e e. Pred ( S , B , b ) si ) )
201 113 ralimi 
 |-  ( A. d e. { a } A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. d e. { a } A. e e. { b } A. f e. Pred ( T , C , c ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
202 162 201 syl 
 |-  ( A. d e. ( Pred ( R , A , a ) u. { a } ) A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. d e. { a } A. e e. { b } A. f e. Pred ( T , C , c ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
203 172 2ralbidv 
 |-  ( d = a -> ( A. e e. { b } A. f e. Pred ( T , C , c ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) <-> A. e e. { b } A. f e. Pred ( T , C , c ) ( ( a =/= a \/ e =/= b \/ f =/= c ) -> ta ) ) )
204 165 203 ralsn 
 |-  ( A. d e. { a } A. e e. { b } A. f e. Pred ( T , C , c ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) <-> A. e e. { b } A. f e. Pred ( T , C , c ) ( ( a =/= a \/ e =/= b \/ f =/= c ) -> ta ) )
205 biidd 
 |-  ( e = b -> ( a =/= a <-> a =/= a ) )
206 205 118 119 3orbi123d 
 |-  ( e = b -> ( ( a =/= a \/ e =/= b \/ f =/= c ) <-> ( a =/= a \/ b =/= b \/ f =/= c ) ) )
207 15 equcoms 
 |-  ( e = b -> ( et <-> ta ) )
208 207 bicomd 
 |-  ( e = b -> ( ta <-> et ) )
209 206 208 imbi12d 
 |-  ( e = b -> ( ( ( a =/= a \/ e =/= b \/ f =/= c ) -> ta ) <-> ( ( a =/= a \/ b =/= b \/ f =/= c ) -> et ) ) )
210 209 ralbidv 
 |-  ( e = b -> ( A. f e. Pred ( T , C , c ) ( ( a =/= a \/ e =/= b \/ f =/= c ) -> ta ) <-> A. f e. Pred ( T , C , c ) ( ( a =/= a \/ b =/= b \/ f =/= c ) -> et ) ) )
211 116 210 ralsn 
 |-  ( A. e e. { b } A. f e. Pred ( T , C , c ) ( ( a =/= a \/ e =/= b \/ f =/= c ) -> ta ) <-> A. f e. Pred ( T , C , c ) ( ( a =/= a \/ b =/= b \/ f =/= c ) -> et ) )
212 204 211 bitri 
 |-  ( A. d e. { a } A. e e. { b } A. f e. Pred ( T , C , c ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) <-> A. f e. Pred ( T , C , c ) ( ( a =/= a \/ b =/= b \/ f =/= c ) -> et ) )
213 202 212 sylib 
 |-  ( A. d e. ( Pred ( R , A , a ) u. { a } ) A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. f e. Pred ( T , C , c ) ( ( a =/= a \/ b =/= b \/ f =/= c ) -> et ) )
214 73 3mix3d 
 |-  ( f e. Pred ( T , C , c ) -> ( a =/= a \/ b =/= b \/ f =/= c ) )
215 pm2.27 
 |-  ( ( a =/= a \/ b =/= b \/ f =/= c ) -> ( ( ( a =/= a \/ b =/= b \/ f =/= c ) -> et ) -> et ) )
216 214 215 syl 
 |-  ( f e. Pred ( T , C , c ) -> ( ( ( a =/= a \/ b =/= b \/ f =/= c ) -> et ) -> et ) )
217 216 ralimia 
 |-  ( A. f e. Pred ( T , C , c ) ( ( a =/= a \/ b =/= b \/ f =/= c ) -> et ) -> A. f e. Pred ( T , C , c ) et )
218 213 217 syl 
 |-  ( A. d e. ( Pred ( R , A , a ) u. { a } ) A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. f e. Pred ( T , C , c ) et )
219 135 200 218 3jca 
 |-  ( A. d e. ( Pred ( R , A , a ) u. { a } ) A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> ( ( A. d e. Pred ( R , A , a ) A. e e. Pred ( S , B , b ) A. f e. Pred ( T , C , c ) th /\ A. d e. Pred ( R , A , a ) A. e e. Pred ( S , B , b ) ch /\ A. d e. Pred ( R , A , a ) A. f e. Pred ( T , C , c ) ze ) /\ ( A. d e. Pred ( R , A , a ) ps /\ A. e e. Pred ( S , B , b ) A. f e. Pred ( T , C , c ) ta /\ A. e e. Pred ( S , B , b ) si ) /\ A. f e. Pred ( T , C , c ) et ) )
220 219 21 syl5 
 |-  ( ( a e. A /\ b e. B /\ c e. C ) -> ( A. d e. ( Pred ( R , A , a ) u. { a } ) A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. ( Pred ( T , C , c ) u. { c } ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> ph ) )
221 56 220 sylbid 
 |-  ( ( a e. A /\ b e. B /\ c e. C ) -> ( A. d A. e A. f ( <. <. d , e >. , f >. e. Pred ( U , ( ( A X. B ) X. C ) , <. <. a , b >. , c >. ) -> th ) -> ph ) )
222 221 11 12 13 18 19 20 frpoins3xp3g 
 |-  ( ( ( U Fr ( ( A X. B ) X. C ) /\ U Po ( ( A X. B ) X. C ) /\ U Se ( ( A X. B ) X. C ) ) /\ ( X e. A /\ Y e. B /\ Z e. C ) ) -> la )
223 37 222 mpan 
 |-  ( ( X e. A /\ Y e. B /\ Z e. C ) -> la )