Metamath Proof Explorer

Theorem xpord3inddlem

Description: Induction over the triple Cartesian product ordering. Note that the substitutions cover all possible cases of membership in the predecessor class. (Contributed by Scott Fenton, 2-Feb-2025)

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 ) ) }
xpord3inddlem.x 
|- ( ka -> X e. A )
xpord3inddlem.y 
|- ( ka -> Y e. B )
xpord3inddlem.z 
|- ( ka -> Z e. C )
xpord3inddlem.1 
|- ( ka -> R Fr A )
xpord3inddlem.2 
|- ( ka -> R Po A )
xpord3inddlem.3 
|- ( ka -> R Se A )
xpord3inddlem.4 
|- ( ka -> S Fr B )
xpord3inddlem.5 
|- ( ka -> S Po B )
xpord3inddlem.6 
|- ( ka -> S Se B )
xpord3inddlem.7 
|- ( ka -> T Fr C )
xpord3inddlem.8 
|- ( ka -> T Po C )
xpord3inddlem.9 
|- ( ka -> T Se C )
xpord3inddlem.10 
|- ( a = d -> ( ph <-> ps ) )
xpord3inddlem.11 
|- ( b = e -> ( ps <-> ch ) )
xpord3inddlem.12 
|- ( c = f -> ( ch <-> th ) )
xpord3inddlem.13 
|- ( a = d -> ( ta <-> th ) )
xpord3inddlem.14 
|- ( b = e -> ( et <-> ta ) )
xpord3inddlem.15 
|- ( b = e -> ( ze <-> th ) )
xpord3inddlem.16 
|- ( c = f -> ( si <-> ta ) )
xpord3inddlem.17 
|- ( a = X -> ( ph <-> rh ) )
xpord3inddlem.18 
|- ( b = Y -> ( rh <-> mu ) )
xpord3inddlem.19 
|- ( c = Z -> ( mu <-> la ) )
xpord3inddlem.i 
|- ( ( ka /\ ( 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 xpord3inddlem 
|- ( ka -> 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 xpord3inddlem.x 
 |-  ( ka -> X e. A )
3 xpord3inddlem.y 
 |-  ( ka -> Y e. B )
4 xpord3inddlem.z 
 |-  ( ka -> Z e. C )
5 xpord3inddlem.1 
 |-  ( ka -> R Fr A )
6 xpord3inddlem.2 
 |-  ( ka -> R Po A )
7 xpord3inddlem.3 
 |-  ( ka -> R Se A )
8 xpord3inddlem.4 
 |-  ( ka -> S Fr B )
9 xpord3inddlem.5 
 |-  ( ka -> S Po B )
10 xpord3inddlem.6 
 |-  ( ka -> S Se B )
11 xpord3inddlem.7 
 |-  ( ka -> T Fr C )
12 xpord3inddlem.8 
 |-  ( ka -> T Po C )
13 xpord3inddlem.9 
 |-  ( ka -> T Se C )
14 xpord3inddlem.10 
 |-  ( a = d -> ( ph <-> ps ) )
15 xpord3inddlem.11 
 |-  ( b = e -> ( ps <-> ch ) )
16 xpord3inddlem.12 
 |-  ( c = f -> ( ch <-> th ) )
17 xpord3inddlem.13 
 |-  ( a = d -> ( ta <-> th ) )
18 xpord3inddlem.14 
 |-  ( b = e -> ( et <-> ta ) )
19 xpord3inddlem.15 
 |-  ( b = e -> ( ze <-> th ) )
20 xpord3inddlem.16 
 |-  ( c = f -> ( si <-> ta ) )
21 xpord3inddlem.17 
 |-  ( a = X -> ( ph <-> rh ) )
22 xpord3inddlem.18 
 |-  ( b = Y -> ( rh <-> mu ) )
23 xpord3inddlem.19 
 |-  ( c = Z -> ( mu <-> la ) )
24 xpord3inddlem.i 
 |-  ( ( ka /\ ( 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 ) )
25 1 5 8 11 frxp3 
 |-  ( ka -> U Fr ( ( A X. B ) X. C ) )
26 1 6 9 12 poxp3 
 |-  ( ka -> U Po ( ( A X. B ) X. C ) )
27 1 7 10 13 sexp3 
 |-  ( ka -> U Se ( ( A X. B ) X. C ) )
28 bi2.04 
 |-  ( ( <. d , e , f >. e. Pred ( U , ( ( A X. B ) X. C ) , <. a , b , c >. ) -> ( ka -> th ) ) <-> ( ka -> ( <. d , e , f >. e. Pred ( U , ( ( A X. B ) X. C ) , <. a , b , c >. ) -> th ) ) )
29 28 3albii 
 |-  ( A. d A. e A. f ( <. d , e , f >. e. Pred ( U , ( ( A X. B ) X. C ) , <. a , b , c >. ) -> ( ka -> th ) ) <-> A. d A. e A. f ( ka -> ( <. d , e , f >. e. Pred ( U , ( ( A X. B ) X. C ) , <. a , b , c >. ) -> th ) ) )
30 19.21v 
 |-  ( A. f ( ka -> ( <. d , e , f >. e. Pred ( U , ( ( A X. B ) X. C ) , <. a , b , c >. ) -> th ) ) <-> ( ka -> A. f ( <. d , e , f >. e. Pred ( U , ( ( A X. B ) X. C ) , <. a , b , c >. ) -> th ) ) )
31 30 2albii 
 |-  ( A. d A. e A. f ( ka -> ( <. d , e , f >. e. Pred ( U , ( ( A X. B ) X. C ) , <. a , b , c >. ) -> th ) ) <-> A. d A. e ( ka -> A. f ( <. d , e , f >. e. Pred ( U , ( ( A X. B ) X. C ) , <. a , b , c >. ) -> th ) ) )
32 19.21v 
 |-  ( A. e ( ka -> A. f ( <. d , e , f >. e. Pred ( U , ( ( A X. B ) X. C ) , <. a , b , c >. ) -> th ) ) <-> ( ka -> A. e A. f ( <. d , e , f >. e. Pred ( U , ( ( A X. B ) X. C ) , <. a , b , c >. ) -> th ) ) )
33 32 albii 
 |-  ( A. d A. e ( ka -> A. f ( <. d , e , f >. e. Pred ( U , ( ( A X. B ) X. C ) , <. a , b , c >. ) -> th ) ) <-> A. d ( ka -> A. e A. f ( <. d , e , f >. e. Pred ( U , ( ( A X. B ) X. C ) , <. a , b , c >. ) -> th ) ) )
34 19.21v 
 |-  ( A. d ( ka -> A. e A. f ( <. d , e , f >. e. Pred ( U , ( ( A X. B ) X. C ) , <. a , b , c >. ) -> th ) ) <-> ( ka -> A. d A. e A. f ( <. d , e , f >. e. Pred ( U , ( ( A X. B ) X. C ) , <. a , b , c >. ) -> th ) ) )
35 33 34 bitri 
 |-  ( A. d A. e ( ka -> A. f ( <. d , e , f >. e. Pred ( U , ( ( A X. B ) X. C ) , <. a , b , c >. ) -> th ) ) <-> ( ka -> A. d A. e A. f ( <. d , e , f >. e. Pred ( U , ( ( A X. B ) X. C ) , <. a , b , c >. ) -> th ) ) )
36 31 35 bitri 
 |-  ( A. d A. e A. f ( ka -> ( <. d , e , f >. e. Pred ( U , ( ( A X. B ) X. C ) , <. a , b , c >. ) -> th ) ) <-> ( ka -> A. d A. e A. f ( <. d , e , f >. e. Pred ( U , ( ( A X. B ) X. C ) , <. a , b , c >. ) -> th ) ) )
37 29 36 bitri 
 |-  ( A. d A. e A. f ( <. d , e , f >. e. Pred ( U , ( ( A X. B ) X. C ) , <. a , b , c >. ) -> ( ka -> th ) ) <-> ( ka -> A. d A. e A. f ( <. d , e , f >. e. Pred ( U , ( ( A X. B ) X. C ) , <. a , b , c >. ) -> th ) ) )
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 adantl 
 |-  ( ( ka /\ ( 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 >. } ) )
40 39 eleq2d 
 |-  ( ( ka /\ ( 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 >. } ) ) )
41 40 imbi1d 
 |-  ( ( ka /\ ( 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 ) ) )
42 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 >. ) )
43 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 } ) ) )
44 vex 
 |-  d e. _V
45 vex 
 |-  e e. _V
46 vex 
 |-  f e. _V
47 44 45 46 otthne 
 |-  ( <. d , e , f >. =/= <. a , b , c >. <-> ( d =/= a \/ e =/= b \/ f =/= c ) )
48 43 47 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 ) ) )
49 42 48 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 ) ) )
50 49 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 ) )
51 41 50 bitrdi 
 |-  ( ( ka /\ ( 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 ) ) )
52 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 ) ) )
53 51 52 bitrdi 
 |-  ( ( ka /\ ( 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 ) ) ) )
54 53 albidv 
 |-  ( ( ka /\ ( 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 ) ) ) )
55 54 2albidv 
 |-  ( ( ka /\ ( 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 ) ) ) )
56 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 ) ) )
57 56 bicomi 
 |-  ( 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 ) ) <-> 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 ) )
58 55 57 bitrdi 
 |-  ( ( ka /\ ( 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 ) ) )
59 ssun1 
 |-  Pred ( T , C , c ) C_ ( Pred ( T , C , c ) u. { c } )
60 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 ) ) )
61 59 60 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 ) )
62 61 ralimi 
 |-  ( 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 ) u. { b } ) A. f e. Pred ( T , C , c ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
63 ssun1 
 |-  Pred ( S , B , b ) C_ ( Pred ( S , B , b ) u. { b } )
64 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 ) ( ( 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 ) ) )
65 63 64 ax-mp 
 |-  ( A. e e. ( Pred ( S , B , b ) u. { 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 ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
66 62 65 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 ) )
67 66 ralimi 
 |-  ( 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 ) u. { a } ) A. e e. Pred ( S , B , b ) A. f e. Pred ( T , C , c ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
68 ssun1 
 |-  Pred ( R , A , a ) C_ ( Pred ( R , A , a ) u. { a } )
69 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 ) 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 ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) ) )
70 68 69 ax-mp 
 |-  ( A. d e. ( Pred ( R , A , a ) u. { 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 ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
71 67 70 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. Pred ( T , C , c ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
72 71 adantl 
 |-  ( ( ka /\ 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 ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
73 predpoirr 
 |-  ( T Po C -> -. c e. Pred ( T , C , c ) )
74 12 73 syl 
 |-  ( ka -> -. c e. Pred ( T , C , c ) )
75 eleq1 
 |-  ( f = c -> ( f e. Pred ( T , C , c ) <-> c e. Pred ( T , C , c ) ) )
76 75 notbid 
 |-  ( f = c -> ( -. f e. Pred ( T , C , c ) <-> -. c e. Pred ( T , C , c ) ) )
77 74 76 syl5ibrcom 
 |-  ( ka -> ( f = c -> -. f e. Pred ( T , C , c ) ) )
78 77 necon2ad 
 |-  ( ka -> ( f e. Pred ( T , C , c ) -> f =/= c ) )
79 78 imp 
 |-  ( ( ka /\ f e. Pred ( T , C , c ) ) -> f =/= c )
80 79 3mix3d 
 |-  ( ( ka /\ f e. Pred ( T , C , c ) ) -> ( d =/= a \/ e =/= b \/ f =/= c ) )
81 pm2.27 
 |-  ( ( d =/= a \/ e =/= b \/ f =/= c ) -> ( ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> th ) )
82 80 81 syl 
 |-  ( ( ka /\ f e. Pred ( T , C , c ) ) -> ( ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> th ) )
83 82 ralimdva 
 |-  ( ka -> ( A. f e. Pred ( T , C , c ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. f e. Pred ( T , C , c ) th ) )
84 83 ralimdv 
 |-  ( ka -> ( 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 ) th ) )
85 84 ralimdv 
 |-  ( ka -> ( 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 ) )
86 85 adantr 
 |-  ( ( ka /\ 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 ) ( ( 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 ) )
87 72 86 mpd 
 |-  ( ( ka /\ 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 )
88 ssun2 
 |-  { c } C_ ( Pred ( T , C , c ) u. { c } )
89 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 ) ) )
90 88 89 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 ) )
91 90 ralimi 
 |-  ( 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 ) u. { b } ) A. f e. { c } ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
92 ssralv 
 |-  ( Pred ( S , B , b ) C_ ( Pred ( S , B , b ) u. { b } ) -> ( A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. { 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 ) ) )
93 63 92 ax-mp 
 |-  ( A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. { 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 ) )
94 91 93 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 ) )
95 94 ralimi 
 |-  ( 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 ) u. { a } ) A. e e. Pred ( S , B , b ) A. f e. { c } ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
96 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 ) 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 ) A. f e. { c } ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) ) )
97 68 96 ax-mp 
 |-  ( A. d e. ( Pred ( R , A , a ) u. { 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 ) A. f e. { c } ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
98 95 97 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 ) )
99 vex 
 |-  c e. _V
100 biidd 
 |-  ( f = c -> ( d =/= a <-> d =/= a ) )
101 biidd 
 |-  ( f = c -> ( e =/= b <-> e =/= b ) )
102 neeq1 
 |-  ( f = c -> ( f =/= c <-> c =/= c ) )
103 100 101 102 3orbi123d 
 |-  ( f = c -> ( ( d =/= a \/ e =/= b \/ f =/= c ) <-> ( d =/= a \/ e =/= b \/ c =/= c ) ) )
104 16 equcoms 
 |-  ( f = c -> ( ch <-> th ) )
105 104 bicomd 
 |-  ( f = c -> ( th <-> ch ) )
106 103 105 imbi12d 
 |-  ( f = c -> ( ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) <-> ( ( d =/= a \/ e =/= b \/ c =/= c ) -> ch ) ) )
107 99 106 ralsn 
 |-  ( A. f e. { c } ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) <-> ( ( d =/= a \/ e =/= b \/ c =/= c ) -> ch ) )
108 107 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 ) )
109 98 108 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 ) )
110 109 adantl 
 |-  ( ( ka /\ 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 ) )
111 predpoirr 
 |-  ( S Po B -> -. b e. Pred ( S , B , b ) )
112 9 111 syl 
 |-  ( ka -> -. b e. Pred ( S , B , b ) )
113 eleq1 
 |-  ( e = b -> ( e e. Pred ( S , B , b ) <-> b e. Pred ( S , B , b ) ) )
114 113 notbid 
 |-  ( e = b -> ( -. e e. Pred ( S , B , b ) <-> -. b e. Pred ( S , B , b ) ) )
115 112 114 syl5ibrcom 
 |-  ( ka -> ( e = b -> -. e e. Pred ( S , B , b ) ) )
116 115 necon2ad 
 |-  ( ka -> ( e e. Pred ( S , B , b ) -> e =/= b ) )
117 116 imp 
 |-  ( ( ka /\ e e. Pred ( S , B , b ) ) -> e =/= b )
118 117 3mix2d 
 |-  ( ( ka /\ e e. Pred ( S , B , b ) ) -> ( d =/= a \/ e =/= b \/ c =/= c ) )
119 pm2.27 
 |-  ( ( d =/= a \/ e =/= b \/ c =/= c ) -> ( ( ( d =/= a \/ e =/= b \/ c =/= c ) -> ch ) -> ch ) )
120 118 119 syl 
 |-  ( ( ka /\ e e. Pred ( S , B , b ) ) -> ( ( ( d =/= a \/ e =/= b \/ c =/= c ) -> ch ) -> ch ) )
121 120 ralimdva 
 |-  ( ka -> ( A. e e. Pred ( S , B , b ) ( ( d =/= a \/ e =/= b \/ c =/= c ) -> ch ) -> A. e e. Pred ( S , B , b ) ch ) )
122 121 ralimdv 
 |-  ( ka -> ( 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 ) )
123 122 adantr 
 |-  ( ( ka /\ 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 ) -> A. d e. Pred ( R , A , a ) A. e e. Pred ( S , B , b ) ch ) )
124 110 123 mpd 
 |-  ( ( ka /\ 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 )
125 ssun2 
 |-  { b } C_ ( Pred ( S , B , b ) u. { b } )
126 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 ) ( ( 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 ) ) )
127 125 126 ax-mp 
 |-  ( A. e e. ( Pred ( S , B , b ) u. { 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 ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
128 62 127 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 ) )
129 128 ralimi 
 |-  ( 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 ) u. { a } ) A. e e. { b } A. f e. Pred ( T , C , c ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
130 ssralv 
 |-  ( Pred ( R , A , a ) C_ ( Pred ( R , A , a ) u. { a } ) -> ( A. d e. ( Pred ( R , A , a ) u. { 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. e e. { b } A. f e. Pred ( T , C , c ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) ) )
131 68 130 ax-mp 
 |-  ( A. d e. ( Pred ( R , A , a ) u. { 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. e e. { b } A. f e. Pred ( T , C , c ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
132 129 131 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 ) )
133 vex 
 |-  b e. _V
134 biidd 
 |-  ( e = b -> ( d =/= a <-> d =/= a ) )
135 neeq1 
 |-  ( e = b -> ( e =/= b <-> b =/= b ) )
136 biidd 
 |-  ( e = b -> ( f =/= c <-> f =/= c ) )
137 134 135 136 3orbi123d 
 |-  ( e = b -> ( ( d =/= a \/ e =/= b \/ f =/= c ) <-> ( d =/= a \/ b =/= b \/ f =/= c ) ) )
138 19 equcoms 
 |-  ( e = b -> ( ze <-> th ) )
139 138 bicomd 
 |-  ( e = b -> ( th <-> ze ) )
140 137 139 imbi12d 
 |-  ( e = b -> ( ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) <-> ( ( d =/= a \/ b =/= b \/ f =/= c ) -> ze ) ) )
141 140 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 ) ) )
142 133 141 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 ) )
143 142 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 ) )
144 132 143 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 ) )
145 144 adantl 
 |-  ( ( ka /\ 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 ) )
146 79 3mix3d 
 |-  ( ( ka /\ f e. Pred ( T , C , c ) ) -> ( d =/= a \/ b =/= b \/ f =/= c ) )
147 pm2.27 
 |-  ( ( d =/= a \/ b =/= b \/ f =/= c ) -> ( ( ( d =/= a \/ b =/= b \/ f =/= c ) -> ze ) -> ze ) )
148 146 147 syl 
 |-  ( ( ka /\ f e. Pred ( T , C , c ) ) -> ( ( ( d =/= a \/ b =/= b \/ f =/= c ) -> ze ) -> ze ) )
149 148 ralimdva 
 |-  ( ka -> ( A. f e. Pred ( T , C , c ) ( ( d =/= a \/ b =/= b \/ f =/= c ) -> ze ) -> A. f e. Pred ( T , C , c ) ze ) )
150 149 ralimdv 
 |-  ( ka -> ( 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 ) )
151 150 adantr 
 |-  ( ( ka /\ 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 ) -> A. d e. Pred ( R , A , a ) A. f e. Pred ( T , C , c ) ze ) )
152 145 151 mpd 
 |-  ( ( ka /\ 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 )
153 87 124 152 3jca 
 |-  ( ( ka /\ 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 ) )
154 ssralv 
 |-  ( { b } C_ ( Pred ( S , B , b ) u. { b } ) -> ( A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. { c } ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. e e. { b } A. f e. { c } ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) ) )
155 125 154 ax-mp 
 |-  ( A. e e. ( Pred ( S , B , b ) u. { b } ) A. f e. { c } ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) -> A. e e. { b } A. f e. { c } ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
156 91 155 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 ) )
157 156 ralimi 
 |-  ( 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 ) u. { a } ) A. e e. { b } A. f e. { c } ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
158 ssralv 
 |-  ( Pred ( R , A , a ) C_ ( Pred ( R , A , a ) u. { a } ) -> ( A. d e. ( Pred ( R , A , a ) u. { a } ) A. e e. { b } A. f e. { 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 ) ) )
159 68 158 ax-mp 
 |-  ( A. d e. ( Pred ( R , A , a ) u. { a } ) A. e e. { b } A. f e. { 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 ) )
160 157 159 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 ) )
161 107 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 ) )
162 biidd 
 |-  ( e = b -> ( c =/= c <-> c =/= c ) )
163 134 135 162 3orbi123d 
 |-  ( e = b -> ( ( d =/= a \/ e =/= b \/ c =/= c ) <-> ( d =/= a \/ b =/= b \/ c =/= c ) ) )
164 15 equcoms 
 |-  ( e = b -> ( ps <-> ch ) )
165 164 bicomd 
 |-  ( e = b -> ( ch <-> ps ) )
166 163 165 imbi12d 
 |-  ( e = b -> ( ( ( d =/= a \/ e =/= b \/ c =/= c ) -> ch ) <-> ( ( d =/= a \/ b =/= b \/ c =/= c ) -> ps ) ) )
167 133 166 ralsn 
 |-  ( A. e e. { b } ( ( d =/= a \/ e =/= b \/ c =/= c ) -> ch ) <-> ( ( d =/= a \/ b =/= b \/ c =/= c ) -> ps ) )
168 161 167 bitri 
 |-  ( A. e e. { b } A. f e. { c } ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) <-> ( ( d =/= a \/ b =/= b \/ c =/= c ) -> ps ) )
169 168 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 ) )
170 160 169 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 ) )
171 170 adantl 
 |-  ( ( ka /\ 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 ) )
172 predpoirr 
 |-  ( R Po A -> -. a e. Pred ( R , A , a ) )
173 6 172 syl 
 |-  ( ka -> -. a e. Pred ( R , A , a ) )
174 eleq1 
 |-  ( d = a -> ( d e. Pred ( R , A , a ) <-> a e. Pred ( R , A , a ) ) )
175 174 notbid 
 |-  ( d = a -> ( -. d e. Pred ( R , A , a ) <-> -. a e. Pred ( R , A , a ) ) )
176 173 175 syl5ibrcom 
 |-  ( ka -> ( d = a -> -. d e. Pred ( R , A , a ) ) )
177 176 necon2ad 
 |-  ( ka -> ( d e. Pred ( R , A , a ) -> d =/= a ) )
178 177 imp 
 |-  ( ( ka /\ d e. Pred ( R , A , a ) ) -> d =/= a )
179 178 3mix1d 
 |-  ( ( ka /\ d e. Pred ( R , A , a ) ) -> ( d =/= a \/ b =/= b \/ c =/= c ) )
180 pm2.27 
 |-  ( ( d =/= a \/ b =/= b \/ c =/= c ) -> ( ( ( d =/= a \/ b =/= b \/ c =/= c ) -> ps ) -> ps ) )
181 179 180 syl 
 |-  ( ( ka /\ d e. Pred ( R , A , a ) ) -> ( ( ( d =/= a \/ b =/= b \/ c =/= c ) -> ps ) -> ps ) )
182 181 ralimdva 
 |-  ( ka -> ( A. d e. Pred ( R , A , a ) ( ( d =/= a \/ b =/= b \/ c =/= c ) -> ps ) -> A. d e. Pred ( R , A , a ) ps ) )
183 182 adantr 
 |-  ( ( ka /\ 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 ) -> A. d e. Pred ( R , A , a ) ps ) )
184 171 183 mpd 
 |-  ( ( ka /\ 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 )
185 ssun2 
 |-  { a } C_ ( Pred ( R , A , a ) u. { a } )
186 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 ) A. f e. Pred ( T , C , 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 ) ) )
187 185 186 ax-mp 
 |-  ( A. d e. ( Pred ( R , A , a ) u. { 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. { a } A. e e. Pred ( S , B , b ) A. f e. Pred ( T , C , c ) ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) )
188 67 187 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 ) )
189 vex 
 |-  a e. _V
190 neeq1 
 |-  ( d = a -> ( d =/= a <-> a =/= a ) )
191 biidd 
 |-  ( d = a -> ( e =/= b <-> e =/= b ) )
192 biidd 
 |-  ( d = a -> ( f =/= c <-> f =/= c ) )
193 190 191 192 3orbi123d 
 |-  ( d = a -> ( ( d =/= a \/ e =/= b \/ f =/= c ) <-> ( a =/= a \/ e =/= b \/ f =/= c ) ) )
194 17 equcoms 
 |-  ( d = a -> ( ta <-> th ) )
195 194 bicomd 
 |-  ( d = a -> ( th <-> ta ) )
196 193 195 imbi12d 
 |-  ( d = a -> ( ( ( d =/= a \/ e =/= b \/ f =/= c ) -> th ) <-> ( ( a =/= a \/ e =/= b \/ f =/= c ) -> ta ) ) )
197 196 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 ) ) )
198 189 197 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 ) )
199 188 198 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 ) )
200 199 adantl 
 |-  ( ( ka /\ 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 ) )
201 79 3mix3d 
 |-  ( ( ka /\ f e. Pred ( T , C , c ) ) -> ( a =/= a \/ e =/= b \/ f =/= c ) )
202 pm2.27 
 |-  ( ( a =/= a \/ e =/= b \/ f =/= c ) -> ( ( ( a =/= a \/ e =/= b \/ f =/= c ) -> ta ) -> ta ) )
203 201 202 syl 
 |-  ( ( ka /\ f e. Pred ( T , C , c ) ) -> ( ( ( a =/= a \/ e =/= b \/ f =/= c ) -> ta ) -> ta ) )
204 203 ralimdva 
 |-  ( ka -> ( A. f e. Pred ( T , C , c ) ( ( a =/= a \/ e =/= b \/ f =/= c ) -> ta ) -> A. f e. Pred ( T , C , c ) ta ) )
205 204 ralimdv 
 |-  ( ka -> ( 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 ) )
206 205 adantr 
 |-  ( ( ka /\ 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 ) -> A. e e. Pred ( S , B , b ) A. f e. Pred ( T , C , c ) ta ) )
207 200 206 mpd 
 |-  ( ( ka /\ 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 )
208 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 ) A. f e. { 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 ) ) )
209 185 208 ax-mp 
 |-  ( A. d e. ( Pred ( R , A , a ) u. { a } ) A. e e. Pred ( S , B , b ) A. f e. { 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 ) )
210 95 209 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 ) )
211 196 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 ) ) )
212 189 211 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 ) )
213 biidd 
 |-  ( f = c -> ( a =/= a <-> a =/= a ) )
214 213 101 102 3orbi123d 
 |-  ( f = c -> ( ( a =/= a \/ e =/= b \/ f =/= c ) <-> ( a =/= a \/ e =/= b \/ c =/= c ) ) )
215 20 bicomd 
 |-  ( c = f -> ( ta <-> si ) )
216 215 equcoms 
 |-  ( f = c -> ( ta <-> si ) )
217 214 216 imbi12d 
 |-  ( f = c -> ( ( ( a =/= a \/ e =/= b \/ f =/= c ) -> ta ) <-> ( ( a =/= a \/ e =/= b \/ c =/= c ) -> si ) ) )
218 99 217 ralsn 
 |-  ( A. f e. { c } ( ( a =/= a \/ e =/= b \/ f =/= c ) -> ta ) <-> ( ( a =/= a \/ e =/= b \/ c =/= c ) -> si ) )
219 218 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 ) )
220 212 219 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 ) )
221 210 220 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 ) )
222 221 adantl 
 |-  ( ( ka /\ 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 ) )
223 117 3mix2d 
 |-  ( ( ka /\ e e. Pred ( S , B , b ) ) -> ( a =/= a \/ e =/= b \/ c =/= c ) )
224 pm2.27 
 |-  ( ( a =/= a \/ e =/= b \/ c =/= c ) -> ( ( ( a =/= a \/ e =/= b \/ c =/= c ) -> si ) -> si ) )
225 223 224 syl 
 |-  ( ( ka /\ e e. Pred ( S , B , b ) ) -> ( ( ( a =/= a \/ e =/= b \/ c =/= c ) -> si ) -> si ) )
226 225 ralimdva 
 |-  ( ka -> ( A. e e. Pred ( S , B , b ) ( ( a =/= a \/ e =/= b \/ c =/= c ) -> si ) -> A. e e. Pred ( S , B , b ) si ) )
227 226 adantr 
 |-  ( ( ka /\ 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 ) -> A. e e. Pred ( S , B , b ) si ) )
228 222 227 mpd 
 |-  ( ( ka /\ 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 )
229 184 207 228 3jca 
 |-  ( ( ka /\ 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 ) )
230 ssralv 
 |-  ( { a } C_ ( Pred ( R , A , a ) u. { a } ) -> ( A. d e. ( Pred ( R , A , a ) u. { a } ) A. e e. { b } A. f e. Pred ( T , C , 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 ) ) )
231 185 230 ax-mp 
 |-  ( A. d e. ( Pred ( R , A , a ) u. { a } ) A. e e. { b } A. f e. Pred ( T , C , 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 ) )
232 129 231 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 ) )
233 196 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 ) ) )
234 189 233 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 ) )
235 biidd 
 |-  ( e = b -> ( a =/= a <-> a =/= a ) )
236 235 135 136 3orbi123d 
 |-  ( e = b -> ( ( a =/= a \/ e =/= b \/ f =/= c ) <-> ( a =/= a \/ b =/= b \/ f =/= c ) ) )
237 equcomi 
 |-  ( e = b -> b = e )
238 bicom1 
 |-  ( ( et <-> ta ) -> ( ta <-> et ) )
239 237 18 238 3syl 
 |-  ( e = b -> ( ta <-> et ) )
240 236 239 imbi12d 
 |-  ( e = b -> ( ( ( a =/= a \/ e =/= b \/ f =/= c ) -> ta ) <-> ( ( a =/= a \/ b =/= b \/ f =/= c ) -> et ) ) )
241 240 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 ) ) )
242 133 241 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 ) )
243 234 242 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 ) )
244 232 243 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 ) )
245 244 adantl 
 |-  ( ( ka /\ 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 ) )
246 79 3mix3d 
 |-  ( ( ka /\ f e. Pred ( T , C , c ) ) -> ( a =/= a \/ b =/= b \/ f =/= c ) )
247 pm2.27 
 |-  ( ( a =/= a \/ b =/= b \/ f =/= c ) -> ( ( ( a =/= a \/ b =/= b \/ f =/= c ) -> et ) -> et ) )
248 246 247 syl 
 |-  ( ( ka /\ f e. Pred ( T , C , c ) ) -> ( ( ( a =/= a \/ b =/= b \/ f =/= c ) -> et ) -> et ) )
249 248 ralimdva 
 |-  ( ka -> ( A. f e. Pred ( T , C , c ) ( ( a =/= a \/ b =/= b \/ f =/= c ) -> et ) -> A. f e. Pred ( T , C , c ) et ) )
250 249 adantr 
 |-  ( ( ka /\ 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 ) -> A. f e. Pred ( T , C , c ) et ) )
251 245 250 mpd 
 |-  ( ( ka /\ 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 )
252 153 229 251 3jca 
 |-  ( ( ka /\ 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 ) )
253 252 ex 
 |-  ( ka -> ( 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 ) ) )
254 253 adantr 
 |-  ( ( ka /\ ( 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 ) -> ( ( 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 ) ) )
255 254 24 syld 
 |-  ( ( ka /\ ( 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 ) )
256 58 255 sylbid 
 |-  ( ( ka /\ ( 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 ) )
257 256 expcom 
 |-  ( ( a e. A /\ b e. B /\ c e. C ) -> ( ka -> ( A. d A. e A. f ( <. d , e , f >. e. Pred ( U , ( ( A X. B ) X. C ) , <. a , b , c >. ) -> th ) -> ph ) ) )
258 257 a2d 
 |-  ( ( a e. A /\ b e. B /\ c e. C ) -> ( ( ka -> A. d A. e A. f ( <. d , e , f >. e. Pred ( U , ( ( A X. B ) X. C ) , <. a , b , c >. ) -> th ) ) -> ( ka -> ph ) ) )
259 37 258 biimtrid 
 |-  ( ( 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 >. ) -> ( ka -> th ) ) -> ( ka -> ph ) ) )
260 14 imbi2d 
 |-  ( a = d -> ( ( ka -> ph ) <-> ( ka -> ps ) ) )
261 15 imbi2d 
 |-  ( b = e -> ( ( ka -> ps ) <-> ( ka -> ch ) ) )
262 16 imbi2d 
 |-  ( c = f -> ( ( ka -> ch ) <-> ( ka -> th ) ) )
263 21 imbi2d 
 |-  ( a = X -> ( ( ka -> ph ) <-> ( ka -> rh ) ) )
264 22 imbi2d 
 |-  ( b = Y -> ( ( ka -> rh ) <-> ( ka -> mu ) ) )
265 23 imbi2d 
 |-  ( c = Z -> ( ( ka -> mu ) <-> ( ka -> la ) ) )
266 259 260 261 262 263 264 265 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 ) ) -> ( ka -> la ) )
267 25 26 27 2 3 4 266 syl33anc 
 |-  ( ka -> ( ka -> la ) )
268 267 pm2.43i 
 |-  ( ka -> la )