Metamath Proof Explorer

Theorem poxp3

Description: Triple Cartesian product partial ordering. (Contributed by Scott Fenton, 21-Aug-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 ) ) }
poxp3.1 
|- ( ph -> R Po A )
poxp3.2 
|- ( ph -> S Po B )
poxp3.3 
|- ( ph -> T Po C )
Assertion poxp3 
|- ( ph -> U Po ( ( A X. B ) X. C ) )

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 poxp3.1 
 |-  ( ph -> R Po A )
3 poxp3.2 
 |-  ( ph -> S Po B )
4 poxp3.3 
 |-  ( ph -> T Po C )
5 el2xptp 
 |-  ( p e. ( ( A X. B ) X. C ) <-> E. a e. A E. b e. B E. c e. C p = <. a , b , c >. )
6 neirr 
 |-  -. a =/= a
7 neirr 
 |-  -. b =/= b
8 neirr 
 |-  -. c =/= c
9 6 7 8 3pm3.2ni 
 |-  -. ( a =/= a \/ b =/= b \/ c =/= c )
10 9 intnan 
 |-  -. ( ( ( a R a \/ a = a ) /\ ( b S b \/ b = b ) /\ ( c T c \/ c = c ) ) /\ ( a =/= a \/ b =/= b \/ c =/= c ) )
11 simp3 
 |-  ( ( ( a e. A /\ b e. B /\ c e. C ) /\ ( a e. A /\ b e. B /\ c e. C ) /\ ( ( ( a R a \/ a = a ) /\ ( b S b \/ b = b ) /\ ( c T c \/ c = c ) ) /\ ( a =/= a \/ b =/= b \/ c =/= c ) ) ) -> ( ( ( a R a \/ a = a ) /\ ( b S b \/ b = b ) /\ ( c T c \/ c = c ) ) /\ ( a =/= a \/ b =/= b \/ c =/= c ) ) )
12 10 11 mto 
 |-  -. ( ( a e. A /\ b e. B /\ c e. C ) /\ ( a e. A /\ b e. B /\ c e. C ) /\ ( ( ( a R a \/ a = a ) /\ ( b S b \/ b = b ) /\ ( c T c \/ c = c ) ) /\ ( a =/= a \/ b =/= b \/ c =/= c ) ) )
13 breq12 
 |-  ( ( p = <. a , b , c >. /\ p = <. a , b , c >. ) -> ( p U p <-> <. a , b , c >. U <. a , b , c >. ) )
14 13 anidms 
 |-  ( p = <. a , b , c >. -> ( p U p <-> <. a , b , c >. U <. a , b , c >. ) )
15 1 xpord3lem 
 |-  ( <. a , b , c >. U <. a , b , c >. <-> ( ( a e. A /\ b e. B /\ c e. C ) /\ ( a e. A /\ b e. B /\ c e. C ) /\ ( ( ( a R a \/ a = a ) /\ ( b S b \/ b = b ) /\ ( c T c \/ c = c ) ) /\ ( a =/= a \/ b =/= b \/ c =/= c ) ) ) )
16 14 15 bitrdi 
 |-  ( p = <. a , b , c >. -> ( p U p <-> ( ( a e. A /\ b e. B /\ c e. C ) /\ ( a e. A /\ b e. B /\ c e. C ) /\ ( ( ( a R a \/ a = a ) /\ ( b S b \/ b = b ) /\ ( c T c \/ c = c ) ) /\ ( a =/= a \/ b =/= b \/ c =/= c ) ) ) ) )
17 12 16 mtbiri 
 |-  ( p = <. a , b , c >. -> -. p U p )
18 17 rexlimivw 
 |-  ( E. c e. C p = <. a , b , c >. -> -. p U p )
19 18 rexlimivw 
 |-  ( E. b e. B E. c e. C p = <. a , b , c >. -> -. p U p )
20 19 rexlimivw 
 |-  ( E. a e. A E. b e. B E. c e. C p = <. a , b , c >. -> -. p U p )
21 5 20 sylbi 
 |-  ( p e. ( ( A X. B ) X. C ) -> -. p U p )
22 21 adantl 
 |-  ( ( ph /\ p e. ( ( A X. B ) X. C ) ) -> -. p U p )
23 3reeanv 
 |-  ( E. a e. A E. d e. A E. g e. A ( E. b e. B E. c e. C p = <. a , b , c >. /\ E. e e. B E. f e. C q = <. d , e , f >. /\ E. h e. B E. i e. C r = <. g , h , i >. ) <-> ( E. a e. A E. b e. B E. c e. C p = <. a , b , c >. /\ E. d e. A E. e e. B E. f e. C q = <. d , e , f >. /\ E. g e. A E. h e. B E. i e. C r = <. g , h , i >. ) )
24 3reeanv 
 |-  ( E. c e. C E. f e. C E. i e. C ( p = <. a , b , c >. /\ q = <. d , e , f >. /\ r = <. g , h , i >. ) <-> ( E. c e. C p = <. a , b , c >. /\ E. f e. C q = <. d , e , f >. /\ E. i e. C r = <. g , h , i >. ) )
25 24 rexbii 
 |-  ( E. h e. B E. c e. C E. f e. C E. i e. C ( p = <. a , b , c >. /\ q = <. d , e , f >. /\ r = <. g , h , i >. ) <-> E. h e. B ( E. c e. C p = <. a , b , c >. /\ E. f e. C q = <. d , e , f >. /\ E. i e. C r = <. g , h , i >. ) )
26 25 2rexbii 
 |-  ( E. b e. B E. e e. B E. h e. B E. c e. C E. f e. C E. i e. C ( p = <. a , b , c >. /\ q = <. d , e , f >. /\ r = <. g , h , i >. ) <-> E. b e. B E. e e. B E. h e. B ( E. c e. C p = <. a , b , c >. /\ E. f e. C q = <. d , e , f >. /\ E. i e. C r = <. g , h , i >. ) )
27 3reeanv 
 |-  ( E. b e. B E. e e. B E. h e. B ( E. c e. C p = <. a , b , c >. /\ E. f e. C q = <. d , e , f >. /\ E. i e. C r = <. g , h , i >. ) <-> ( E. b e. B E. c e. C p = <. a , b , c >. /\ E. e e. B E. f e. C q = <. d , e , f >. /\ E. h e. B E. i e. C r = <. g , h , i >. ) )
28 26 27 bitri 
 |-  ( E. b e. B E. e e. B E. h e. B E. c e. C E. f e. C E. i e. C ( p = <. a , b , c >. /\ q = <. d , e , f >. /\ r = <. g , h , i >. ) <-> ( E. b e. B E. c e. C p = <. a , b , c >. /\ E. e e. B E. f e. C q = <. d , e , f >. /\ E. h e. B E. i e. C r = <. g , h , i >. ) )
29 28 rexbii 
 |-  ( E. g e. A E. b e. B E. e e. B E. h e. B E. c e. C E. f e. C E. i e. C ( p = <. a , b , c >. /\ q = <. d , e , f >. /\ r = <. g , h , i >. ) <-> E. g e. A ( E. b e. B E. c e. C p = <. a , b , c >. /\ E. e e. B E. f e. C q = <. d , e , f >. /\ E. h e. B E. i e. C r = <. g , h , i >. ) )
30 29 2rexbii 
 |-  ( E. a e. A E. d e. A E. g e. A E. b e. B E. e e. B E. h e. B E. c e. C E. f e. C E. i e. C ( p = <. a , b , c >. /\ q = <. d , e , f >. /\ r = <. g , h , i >. ) <-> E. a e. A E. d e. A E. g e. A ( E. b e. B E. c e. C p = <. a , b , c >. /\ E. e e. B E. f e. C q = <. d , e , f >. /\ E. h e. B E. i e. C r = <. g , h , i >. ) )
31 el2xptp 
 |-  ( q e. ( ( A X. B ) X. C ) <-> E. d e. A E. e e. B E. f e. C q = <. d , e , f >. )
32 el2xptp 
 |-  ( r e. ( ( A X. B ) X. C ) <-> E. g e. A E. h e. B E. i e. C r = <. g , h , i >. )
33 5 31 32 3anbi123i 
 |-  ( ( p e. ( ( A X. B ) X. C ) /\ q e. ( ( A X. B ) X. C ) /\ r e. ( ( A X. B ) X. C ) ) <-> ( E. a e. A E. b e. B E. c e. C p = <. a , b , c >. /\ E. d e. A E. e e. B E. f e. C q = <. d , e , f >. /\ E. g e. A E. h e. B E. i e. C r = <. g , h , i >. ) )
34 23 30 33 3bitr4ri 
 |-  ( ( p e. ( ( A X. B ) X. C ) /\ q e. ( ( A X. B ) X. C ) /\ r e. ( ( A X. B ) X. C ) ) <-> E. a e. A E. d e. A E. g e. A E. b e. B E. e e. B E. h e. B E. c e. C E. f e. C E. i e. C ( p = <. a , b , c >. /\ q = <. d , e , f >. /\ r = <. g , h , i >. ) )
35 simpr1l 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( a e. A /\ b e. B /\ c e. C ) )
36 simpr2r 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( g e. A /\ h e. B /\ i e. C ) )
37 simp1l1 
 |-  ( ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) -> a e. A )
38 simp2l1 
 |-  ( ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) -> d e. A )
39 simp2r1 
 |-  ( ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) -> g e. A )
40 37 38 39 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) -> ( a e. A /\ d e. A /\ g e. A ) )
41 potr 
 |-  ( ( R Po A /\ ( a e. A /\ d e. A /\ g e. A ) ) -> ( ( a R d /\ d R g ) -> a R g ) )
42 2 40 41 syl2an 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( ( a R d /\ d R g ) -> a R g ) )
43 42 expd 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( a R d -> ( d R g -> a R g ) ) )
44 breq1 
 |-  ( a = d -> ( a R g <-> d R g ) )
45 44 biimprd 
 |-  ( a = d -> ( d R g -> a R g ) )
46 45 a1i 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( a = d -> ( d R g -> a R g ) ) )
47 simpll1 
 |-  ( ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) -> ( a R d \/ a = d ) )
48 47 3ad2ant3 
 |-  ( ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) -> ( a R d \/ a = d ) )
49 48 adantl 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( a R d \/ a = d ) )
50 43 46 49 mpjaod 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( d R g -> a R g ) )
51 orc 
 |-  ( a R g -> ( a R g \/ a = g ) )
52 50 51 syl6 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( d R g -> ( a R g \/ a = g ) ) )
53 breq2 
 |-  ( d = g -> ( a R d <-> a R g ) )
54 equequ2 
 |-  ( d = g -> ( a = d <-> a = g ) )
55 53 54 orbi12d 
 |-  ( d = g -> ( ( a R d \/ a = d ) <-> ( a R g \/ a = g ) ) )
56 49 55 syl5ibcom 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( d = g -> ( a R g \/ a = g ) ) )
57 simprl1 
 |-  ( ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) -> ( d R g \/ d = g ) )
58 57 3ad2ant3 
 |-  ( ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) -> ( d R g \/ d = g ) )
59 58 adantl 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( d R g \/ d = g ) )
60 52 56 59 mpjaod 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( a R g \/ a = g ) )
61 simp1l2 
 |-  ( ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) -> b e. B )
62 simp2l2 
 |-  ( ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) -> e e. B )
63 simp2r2 
 |-  ( ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) -> h e. B )
64 61 62 63 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) -> ( b e. B /\ e e. B /\ h e. B ) )
65 potr 
 |-  ( ( S Po B /\ ( b e. B /\ e e. B /\ h e. B ) ) -> ( ( b S e /\ e S h ) -> b S h ) )
66 3 64 65 syl2an 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( ( b S e /\ e S h ) -> b S h ) )
67 66 expd 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( b S e -> ( e S h -> b S h ) ) )
68 breq1 
 |-  ( b = e -> ( b S h <-> e S h ) )
69 68 biimprd 
 |-  ( b = e -> ( e S h -> b S h ) )
70 69 a1i 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( b = e -> ( e S h -> b S h ) ) )
71 simpll2 
 |-  ( ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) -> ( b S e \/ b = e ) )
72 71 3ad2ant3 
 |-  ( ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) -> ( b S e \/ b = e ) )
73 72 adantl 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( b S e \/ b = e ) )
74 67 70 73 mpjaod 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( e S h -> b S h ) )
75 orc 
 |-  ( b S h -> ( b S h \/ b = h ) )
76 74 75 syl6 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( e S h -> ( b S h \/ b = h ) ) )
77 breq2 
 |-  ( e = h -> ( b S e <-> b S h ) )
78 equequ2 
 |-  ( e = h -> ( b = e <-> b = h ) )
79 77 78 orbi12d 
 |-  ( e = h -> ( ( b S e \/ b = e ) <-> ( b S h \/ b = h ) ) )
80 73 79 syl5ibcom 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( e = h -> ( b S h \/ b = h ) ) )
81 simprl2 
 |-  ( ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) -> ( e S h \/ e = h ) )
82 81 3ad2ant3 
 |-  ( ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) -> ( e S h \/ e = h ) )
83 82 adantl 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( e S h \/ e = h ) )
84 76 80 83 mpjaod 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( b S h \/ b = h ) )
85 simp1l3 
 |-  ( ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) -> c e. C )
86 simp2l3 
 |-  ( ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) -> f e. C )
87 simp2r3 
 |-  ( ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) -> i e. C )
88 85 86 87 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) -> ( c e. C /\ f e. C /\ i e. C ) )
89 potr 
 |-  ( ( T Po C /\ ( c e. C /\ f e. C /\ i e. C ) ) -> ( ( c T f /\ f T i ) -> c T i ) )
90 4 88 89 syl2an 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( ( c T f /\ f T i ) -> c T i ) )
91 90 expd 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( c T f -> ( f T i -> c T i ) ) )
92 breq1 
 |-  ( c = f -> ( c T i <-> f T i ) )
93 92 biimprd 
 |-  ( c = f -> ( f T i -> c T i ) )
94 93 a1i 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( c = f -> ( f T i -> c T i ) ) )
95 simpll3 
 |-  ( ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) -> ( c T f \/ c = f ) )
96 95 3ad2ant3 
 |-  ( ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) -> ( c T f \/ c = f ) )
97 96 adantl 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( c T f \/ c = f ) )
98 91 94 97 mpjaod 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( f T i -> c T i ) )
99 orc 
 |-  ( c T i -> ( c T i \/ c = i ) )
100 98 99 syl6 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( f T i -> ( c T i \/ c = i ) ) )
101 breq2 
 |-  ( f = i -> ( c T f <-> c T i ) )
102 equequ2 
 |-  ( f = i -> ( c = f <-> c = i ) )
103 101 102 orbi12d 
 |-  ( f = i -> ( ( c T f \/ c = f ) <-> ( c T i \/ c = i ) ) )
104 97 103 syl5ibcom 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( f = i -> ( c T i \/ c = i ) ) )
105 simprl3 
 |-  ( ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) -> ( f T i \/ f = i ) )
106 105 3ad2ant3 
 |-  ( ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) -> ( f T i \/ f = i ) )
107 106 adantl 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( f T i \/ f = i ) )
108 100 104 107 mpjaod 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( c T i \/ c = i ) )
109 60 84 108 3jca 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( ( a R g \/ a = g ) /\ ( b S h \/ b = h ) /\ ( c T i \/ c = i ) ) )
110 simp3rr 
 |-  ( ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) -> ( d =/= g \/ e =/= h \/ f =/= i ) )
111 110 adantl 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( d =/= g \/ e =/= h \/ f =/= i ) )
112 59 adantr 
 |-  ( ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) /\ a = g ) -> ( d R g \/ d = g ) )
113 breq1 
 |-  ( a = g -> ( a R d <-> g R d ) )
114 equequ1 
 |-  ( a = g -> ( a = d <-> g = d ) )
115 equcom 
 |-  ( g = d <-> d = g )
116 114 115 bitrdi 
 |-  ( a = g -> ( a = d <-> d = g ) )
117 113 116 orbi12d 
 |-  ( a = g -> ( ( a R d \/ a = d ) <-> ( g R d \/ d = g ) ) )
118 49 117 syl5ibcom 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( a = g -> ( g R d \/ d = g ) ) )
119 118 imp 
 |-  ( ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) /\ a = g ) -> ( g R d \/ d = g ) )
120 ordir 
 |-  ( ( ( d R g /\ g R d ) \/ d = g ) <-> ( ( d R g \/ d = g ) /\ ( g R d \/ d = g ) ) )
121 112 119 120 sylanbrc 
 |-  ( ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) /\ a = g ) -> ( ( d R g /\ g R d ) \/ d = g ) )
122 2 adantr 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> R Po A )
123 38 adantl 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> d e. A )
124 39 adantl 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> g e. A )
125 po2nr 
 |-  ( ( R Po A /\ ( d e. A /\ g e. A ) ) -> -. ( d R g /\ g R d ) )
126 122 123 124 125 syl12anc 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> -. ( d R g /\ g R d ) )
127 126 adantr 
 |-  ( ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) /\ a = g ) -> -. ( d R g /\ g R d ) )
128 121 127 orcnd 
 |-  ( ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) /\ a = g ) -> d = g )
129 128 ex 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( a = g -> d = g ) )
130 129 necon3d 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( d =/= g -> a =/= g ) )
131 83 adantr 
 |-  ( ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) /\ b = h ) -> ( e S h \/ e = h ) )
132 breq1 
 |-  ( b = h -> ( b S e <-> h S e ) )
133 equequ1 
 |-  ( b = h -> ( b = e <-> h = e ) )
134 equcom 
 |-  ( h = e <-> e = h )
135 133 134 bitrdi 
 |-  ( b = h -> ( b = e <-> e = h ) )
136 132 135 orbi12d 
 |-  ( b = h -> ( ( b S e \/ b = e ) <-> ( h S e \/ e = h ) ) )
137 73 136 syl5ibcom 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( b = h -> ( h S e \/ e = h ) ) )
138 137 imp 
 |-  ( ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) /\ b = h ) -> ( h S e \/ e = h ) )
139 ordir 
 |-  ( ( ( e S h /\ h S e ) \/ e = h ) <-> ( ( e S h \/ e = h ) /\ ( h S e \/ e = h ) ) )
140 131 138 139 sylanbrc 
 |-  ( ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) /\ b = h ) -> ( ( e S h /\ h S e ) \/ e = h ) )
141 3 adantr 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> S Po B )
142 62 adantl 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> e e. B )
143 63 adantl 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> h e. B )
144 po2nr 
 |-  ( ( S Po B /\ ( e e. B /\ h e. B ) ) -> -. ( e S h /\ h S e ) )
145 141 142 143 144 syl12anc 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> -. ( e S h /\ h S e ) )
146 145 adantr 
 |-  ( ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) /\ b = h ) -> -. ( e S h /\ h S e ) )
147 140 146 orcnd 
 |-  ( ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) /\ b = h ) -> e = h )
148 147 ex 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( b = h -> e = h ) )
149 148 necon3d 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( e =/= h -> b =/= h ) )
150 107 adantr 
 |-  ( ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) /\ c = i ) -> ( f T i \/ f = i ) )
151 breq1 
 |-  ( c = i -> ( c T f <-> i T f ) )
152 equequ1 
 |-  ( c = i -> ( c = f <-> i = f ) )
153 equcom 
 |-  ( i = f <-> f = i )
154 152 153 bitrdi 
 |-  ( c = i -> ( c = f <-> f = i ) )
155 151 154 orbi12d 
 |-  ( c = i -> ( ( c T f \/ c = f ) <-> ( i T f \/ f = i ) ) )
156 97 155 syl5ibcom 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( c = i -> ( i T f \/ f = i ) ) )
157 156 imp 
 |-  ( ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) /\ c = i ) -> ( i T f \/ f = i ) )
158 ordir 
 |-  ( ( ( f T i /\ i T f ) \/ f = i ) <-> ( ( f T i \/ f = i ) /\ ( i T f \/ f = i ) ) )
159 150 157 158 sylanbrc 
 |-  ( ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) /\ c = i ) -> ( ( f T i /\ i T f ) \/ f = i ) )
160 4 adantr 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> T Po C )
161 86 adantl 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> f e. C )
162 87 adantl 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> i e. C )
163 po2nr 
 |-  ( ( T Po C /\ ( f e. C /\ i e. C ) ) -> -. ( f T i /\ i T f ) )
164 160 161 162 163 syl12anc 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> -. ( f T i /\ i T f ) )
165 164 adantr 
 |-  ( ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) /\ c = i ) -> -. ( f T i /\ i T f ) )
166 159 165 orcnd 
 |-  ( ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) /\ c = i ) -> f = i )
167 166 ex 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( c = i -> f = i ) )
168 167 necon3d 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( f =/= i -> c =/= i ) )
169 130 149 168 3orim123d 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( ( d =/= g \/ e =/= h \/ f =/= i ) -> ( a =/= g \/ b =/= h \/ c =/= i ) ) )
170 111 169 mpd 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( a =/= g \/ b =/= h \/ c =/= i ) )
171 109 170 jca 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( ( ( a R g \/ a = g ) /\ ( b S h \/ b = h ) /\ ( c T i \/ c = i ) ) /\ ( a =/= g \/ b =/= h \/ c =/= i ) ) )
172 35 36 171 3jca 
 |-  ( ( ph /\ ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) -> ( ( a e. A /\ b e. B /\ c e. C ) /\ ( g e. A /\ h e. B /\ i e. C ) /\ ( ( ( a R g \/ a = g ) /\ ( b S h \/ b = h ) /\ ( c T i \/ c = i ) ) /\ ( a =/= g \/ b =/= h \/ c =/= i ) ) ) )
173 172 ex 
 |-  ( ph -> ( ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) -> ( ( a e. A /\ b e. B /\ c e. C ) /\ ( g e. A /\ h e. B /\ i e. C ) /\ ( ( ( a R g \/ a = g ) /\ ( b S h \/ b = h ) /\ ( c T i \/ c = i ) ) /\ ( a =/= g \/ b =/= h \/ c =/= i ) ) ) ) )
174 breq12 
 |-  ( ( p = <. a , b , c >. /\ q = <. d , e , f >. ) -> ( p U q <-> <. a , b , c >. U <. d , e , f >. ) )
175 174 3adant3 
 |-  ( ( p = <. a , b , c >. /\ q = <. d , e , f >. /\ r = <. g , h , i >. ) -> ( p U q <-> <. a , b , c >. U <. d , e , f >. ) )
176 1 xpord3lem 
 |-  ( <. a , b , c >. U <. d , e , f >. <-> ( ( a e. A /\ b e. B /\ c e. C ) /\ ( d e. A /\ e e. B /\ f e. C ) /\ ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) ) )
177 175 176 bitrdi 
 |-  ( ( p = <. a , b , c >. /\ q = <. d , e , f >. /\ r = <. g , h , i >. ) -> ( p U q <-> ( ( a e. A /\ b e. B /\ c e. C ) /\ ( d e. A /\ e e. B /\ f e. C ) /\ ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) ) ) )
178 breq12 
 |-  ( ( q = <. d , e , f >. /\ r = <. g , h , i >. ) -> ( q U r <-> <. d , e , f >. U <. g , h , i >. ) )
179 178 3adant1 
 |-  ( ( p = <. a , b , c >. /\ q = <. d , e , f >. /\ r = <. g , h , i >. ) -> ( q U r <-> <. d , e , f >. U <. g , h , i >. ) )
180 1 xpord3lem 
 |-  ( <. d , e , f >. U <. g , h , i >. <-> ( ( d e. A /\ e e. B /\ f e. C ) /\ ( g e. A /\ h e. B /\ i e. C ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) )
181 179 180 bitrdi 
 |-  ( ( p = <. a , b , c >. /\ q = <. d , e , f >. /\ r = <. g , h , i >. ) -> ( q U r <-> ( ( d e. A /\ e e. B /\ f e. C ) /\ ( g e. A /\ h e. B /\ i e. C ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) )
182 177 181 anbi12d 
 |-  ( ( p = <. a , b , c >. /\ q = <. d , e , f >. /\ r = <. g , h , i >. ) -> ( ( p U q /\ q U r ) <-> ( ( ( a e. A /\ b e. B /\ c e. C ) /\ ( d e. A /\ e e. B /\ f e. C ) /\ ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) ) /\ ( ( d e. A /\ e e. B /\ f e. C ) /\ ( g e. A /\ h e. B /\ i e. C ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) )
183 an6 
 |-  ( ( ( ( a e. A /\ b e. B /\ c e. C ) /\ ( d e. A /\ e e. B /\ f e. C ) /\ ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) ) /\ ( ( d e. A /\ e e. B /\ f e. C ) /\ ( g e. A /\ h e. B /\ i e. C ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) <-> ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) )
184 182 183 bitrdi 
 |-  ( ( p = <. a , b , c >. /\ q = <. d , e , f >. /\ r = <. g , h , i >. ) -> ( ( p U q /\ q U r ) <-> ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) ) )
185 breq12 
 |-  ( ( p = <. a , b , c >. /\ r = <. g , h , i >. ) -> ( p U r <-> <. a , b , c >. U <. g , h , i >. ) )
186 185 3adant2 
 |-  ( ( p = <. a , b , c >. /\ q = <. d , e , f >. /\ r = <. g , h , i >. ) -> ( p U r <-> <. a , b , c >. U <. g , h , i >. ) )
187 1 xpord3lem 
 |-  ( <. a , b , c >. U <. g , h , i >. <-> ( ( a e. A /\ b e. B /\ c e. C ) /\ ( g e. A /\ h e. B /\ i e. C ) /\ ( ( ( a R g \/ a = g ) /\ ( b S h \/ b = h ) /\ ( c T i \/ c = i ) ) /\ ( a =/= g \/ b =/= h \/ c =/= i ) ) ) )
188 186 187 bitrdi 
 |-  ( ( p = <. a , b , c >. /\ q = <. d , e , f >. /\ r = <. g , h , i >. ) -> ( p U r <-> ( ( a e. A /\ b e. B /\ c e. C ) /\ ( g e. A /\ h e. B /\ i e. C ) /\ ( ( ( a R g \/ a = g ) /\ ( b S h \/ b = h ) /\ ( c T i \/ c = i ) ) /\ ( a =/= g \/ b =/= h \/ c =/= i ) ) ) ) )
189 184 188 imbi12d 
 |-  ( ( p = <. a , b , c >. /\ q = <. d , e , f >. /\ r = <. g , h , i >. ) -> ( ( ( p U q /\ q U r ) -> p U r ) <-> ( ( ( ( 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 ) /\ ( g e. A /\ h e. B /\ i e. C ) ) /\ ( ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) /\ ( ( ( d R g \/ d = g ) /\ ( e S h \/ e = h ) /\ ( f T i \/ f = i ) ) /\ ( d =/= g \/ e =/= h \/ f =/= i ) ) ) ) -> ( ( a e. A /\ b e. B /\ c e. C ) /\ ( g e. A /\ h e. B /\ i e. C ) /\ ( ( ( a R g \/ a = g ) /\ ( b S h \/ b = h ) /\ ( c T i \/ c = i ) ) /\ ( a =/= g \/ b =/= h \/ c =/= i ) ) ) ) ) )
190 173 189 syl5ibrcom 
 |-  ( ph -> ( ( p = <. a , b , c >. /\ q = <. d , e , f >. /\ r = <. g , h , i >. ) -> ( ( p U q /\ q U r ) -> p U r ) ) )
191 190 rexlimdvw 
 |-  ( ph -> ( E. i e. C ( p = <. a , b , c >. /\ q = <. d , e , f >. /\ r = <. g , h , i >. ) -> ( ( p U q /\ q U r ) -> p U r ) ) )
192 191 rexlimdvw 
 |-  ( ph -> ( E. f e. C E. i e. C ( p = <. a , b , c >. /\ q = <. d , e , f >. /\ r = <. g , h , i >. ) -> ( ( p U q /\ q U r ) -> p U r ) ) )
193 192 rexlimdvw 
 |-  ( ph -> ( E. c e. C E. f e. C E. i e. C ( p = <. a , b , c >. /\ q = <. d , e , f >. /\ r = <. g , h , i >. ) -> ( ( p U q /\ q U r ) -> p U r ) ) )
194 193 rexlimdvw 
 |-  ( ph -> ( E. h e. B E. c e. C E. f e. C E. i e. C ( p = <. a , b , c >. /\ q = <. d , e , f >. /\ r = <. g , h , i >. ) -> ( ( p U q /\ q U r ) -> p U r ) ) )
195 194 rexlimdvw 
 |-  ( ph -> ( E. e e. B E. h e. B E. c e. C E. f e. C E. i e. C ( p = <. a , b , c >. /\ q = <. d , e , f >. /\ r = <. g , h , i >. ) -> ( ( p U q /\ q U r ) -> p U r ) ) )
196 195 rexlimdvw 
 |-  ( ph -> ( E. b e. B E. e e. B E. h e. B E. c e. C E. f e. C E. i e. C ( p = <. a , b , c >. /\ q = <. d , e , f >. /\ r = <. g , h , i >. ) -> ( ( p U q /\ q U r ) -> p U r ) ) )
197 196 rexlimdvw 
 |-  ( ph -> ( E. g e. A E. b e. B E. e e. B E. h e. B E. c e. C E. f e. C E. i e. C ( p = <. a , b , c >. /\ q = <. d , e , f >. /\ r = <. g , h , i >. ) -> ( ( p U q /\ q U r ) -> p U r ) ) )
198 197 rexlimdvw 
 |-  ( ph -> ( E. d e. A E. g e. A E. b e. B E. e e. B E. h e. B E. c e. C E. f e. C E. i e. C ( p = <. a , b , c >. /\ q = <. d , e , f >. /\ r = <. g , h , i >. ) -> ( ( p U q /\ q U r ) -> p U r ) ) )
199 198 rexlimdvw 
 |-  ( ph -> ( E. a e. A E. d e. A E. g e. A E. b e. B E. e e. B E. h e. B E. c e. C E. f e. C E. i e. C ( p = <. a , b , c >. /\ q = <. d , e , f >. /\ r = <. g , h , i >. ) -> ( ( p U q /\ q U r ) -> p U r ) ) )
200 34 199 biimtrid 
 |-  ( ph -> ( ( p e. ( ( A X. B ) X. C ) /\ q e. ( ( A X. B ) X. C ) /\ r e. ( ( A X. B ) X. C ) ) -> ( ( p U q /\ q U r ) -> p U r ) ) )
201 200 imp 
 |-  ( ( ph /\ ( p e. ( ( A X. B ) X. C ) /\ q e. ( ( A X. B ) X. C ) /\ r e. ( ( A X. B ) X. C ) ) ) -> ( ( p U q /\ q U r ) -> p U r ) )
202 22 201 ispod 
 |-  ( ph -> U Po ( ( A X. B ) X. C ) )