Metamath Proof Explorer

Theorem poxp3

Description: Triple cross 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 elxpxp 
 |-  ( a e. ( ( A X. B ) X. C ) <-> E. d e. A E. e e. B E. f e. C a = <. <. d , e >. , f >. )
6 neirr 
 |-  -. d =/= d
7 neirr 
 |-  -. e =/= e
8 neirr 
 |-  -. f =/= f
9 6 7 8 3pm3.2ni 
 |-  -. ( d =/= d \/ e =/= e \/ f =/= f )
10 9 intnan 
 |-  -. ( ( ( d R d \/ d = d ) /\ ( e S e \/ e = e ) /\ ( f T f \/ f = f ) ) /\ ( d =/= d \/ e =/= e \/ f =/= f ) )
11 simp3 
 |-  ( ( ( d e. A /\ e e. B /\ f e. C ) /\ ( d e. A /\ e e. B /\ f e. C ) /\ ( ( ( d R d \/ d = d ) /\ ( e S e \/ e = e ) /\ ( f T f \/ f = f ) ) /\ ( d =/= d \/ e =/= e \/ f =/= f ) ) ) -> ( ( ( d R d \/ d = d ) /\ ( e S e \/ e = e ) /\ ( f T f \/ f = f ) ) /\ ( d =/= d \/ e =/= e \/ f =/= f ) ) )
12 10 11 mto 
 |-  -. ( ( d e. A /\ e e. B /\ f e. C ) /\ ( d e. A /\ e e. B /\ f e. C ) /\ ( ( ( d R d \/ d = d ) /\ ( e S e \/ e = e ) /\ ( f T f \/ f = f ) ) /\ ( d =/= d \/ e =/= e \/ f =/= f ) ) )
13 breq12 
 |-  ( ( a = <. <. d , e >. , f >. /\ a = <. <. d , e >. , f >. ) -> ( a U a <-> <. <. d , e >. , f >. U <. <. d , e >. , f >. ) )
14 13 anidms 
 |-  ( a = <. <. d , e >. , f >. -> ( a U a <-> <. <. d , e >. , f >. U <. <. d , e >. , f >. ) )
15 1 xpord3lem 
 |-  ( <. <. d , e >. , f >. U <. <. d , e >. , f >. <-> ( ( d e. A /\ e e. B /\ f e. C ) /\ ( d e. A /\ e e. B /\ f e. C ) /\ ( ( ( d R d \/ d = d ) /\ ( e S e \/ e = e ) /\ ( f T f \/ f = f ) ) /\ ( d =/= d \/ e =/= e \/ f =/= f ) ) ) )
16 14 15 bitrdi 
 |-  ( a = <. <. d , e >. , f >. -> ( a U a <-> ( ( d e. A /\ e e. B /\ f e. C ) /\ ( d e. A /\ e e. B /\ f e. C ) /\ ( ( ( d R d \/ d = d ) /\ ( e S e \/ e = e ) /\ ( f T f \/ f = f ) ) /\ ( d =/= d \/ e =/= e \/ f =/= f ) ) ) ) )
17 12 16 mtbiri 
 |-  ( a = <. <. d , e >. , f >. -> -. a U a )
18 17 rexlimivw 
 |-  ( E. f e. C a = <. <. d , e >. , f >. -> -. a U a )
19 18 a1i 
 |-  ( ( d e. A /\ e e. B ) -> ( E. f e. C a = <. <. d , e >. , f >. -> -. a U a ) )
20 19 rexlimivv 
 |-  ( E. d e. A E. e e. B E. f e. C a = <. <. d , e >. , f >. -> -. a U a )
21 5 20 sylbi 
 |-  ( a e. ( ( A X. B ) X. C ) -> -. a U a )
22 21 adantl 
 |-  ( ( ph /\ a e. ( ( A X. B ) X. C ) ) -> -. a U a )
23 elxpxp 
 |-  ( b e. ( ( A X. B ) X. C ) <-> E. g e. A E. h e. B E. i e. C b = <. <. g , h >. , i >. )
24 elxpxp 
 |-  ( c e. ( ( A X. B ) X. C ) <-> E. j e. A E. k e. B E. l e. C c = <. <. j , k >. , l >. )
25 5 23 24 3anbi123i 
 |-  ( ( a e. ( ( A X. B ) X. C ) /\ b e. ( ( A X. B ) X. C ) /\ c e. ( ( A X. B ) X. C ) ) <-> ( E. d e. A E. e e. B E. f e. C a = <. <. d , e >. , f >. /\ E. g e. A E. h e. B E. i e. C b = <. <. g , h >. , i >. /\ E. j e. A E. k e. B E. l e. C c = <. <. j , k >. , l >. ) )
26 3reeanv 
 |-  ( E. f e. C E. i e. C E. l e. C ( a = <. <. d , e >. , f >. /\ b = <. <. g , h >. , i >. /\ c = <. <. j , k >. , l >. ) <-> ( E. f e. C a = <. <. d , e >. , f >. /\ E. i e. C b = <. <. g , h >. , i >. /\ E. l e. C c = <. <. j , k >. , l >. ) )
27 26 rexbii 
 |-  ( E. k e. B E. f e. C E. i e. C E. l e. C ( a = <. <. d , e >. , f >. /\ b = <. <. g , h >. , i >. /\ c = <. <. j , k >. , l >. ) <-> E. k e. B ( E. f e. C a = <. <. d , e >. , f >. /\ E. i e. C b = <. <. g , h >. , i >. /\ E. l e. C c = <. <. j , k >. , l >. ) )
28 27 2rexbii 
 |-  ( E. e e. B E. h e. B E. k e. B E. f e. C E. i e. C E. l e. C ( a = <. <. d , e >. , f >. /\ b = <. <. g , h >. , i >. /\ c = <. <. j , k >. , l >. ) <-> E. e e. B E. h e. B E. k e. B ( E. f e. C a = <. <. d , e >. , f >. /\ E. i e. C b = <. <. g , h >. , i >. /\ E. l e. C c = <. <. j , k >. , l >. ) )
29 3reeanv 
 |-  ( E. e e. B E. h e. B E. k e. B ( E. f e. C a = <. <. d , e >. , f >. /\ E. i e. C b = <. <. g , h >. , i >. /\ E. l e. C c = <. <. j , k >. , l >. ) <-> ( E. e e. B E. f e. C a = <. <. d , e >. , f >. /\ E. h e. B E. i e. C b = <. <. g , h >. , i >. /\ E. k e. B E. l e. C c = <. <. j , k >. , l >. ) )
30 28 29 bitri 
 |-  ( E. e e. B E. h e. B E. k e. B E. f e. C E. i e. C E. l e. C ( a = <. <. d , e >. , f >. /\ b = <. <. g , h >. , i >. /\ c = <. <. j , k >. , l >. ) <-> ( E. e e. B E. f e. C a = <. <. d , e >. , f >. /\ E. h e. B E. i e. C b = <. <. g , h >. , i >. /\ E. k e. B E. l e. C c = <. <. j , k >. , l >. ) )
31 30 rexbii 
 |-  ( E. j e. A E. e e. B E. h e. B E. k e. B E. f e. C E. i e. C E. l e. C ( a = <. <. d , e >. , f >. /\ b = <. <. g , h >. , i >. /\ c = <. <. j , k >. , l >. ) <-> E. j e. A ( E. e e. B E. f e. C a = <. <. d , e >. , f >. /\ E. h e. B E. i e. C b = <. <. g , h >. , i >. /\ E. k e. B E. l e. C c = <. <. j , k >. , l >. ) )
32 31 2rexbii 
 |-  ( E. d e. A E. g e. A E. j e. A E. e e. B E. h e. B E. k e. B E. f e. C E. i e. C E. l e. C ( a = <. <. d , e >. , f >. /\ b = <. <. g , h >. , i >. /\ c = <. <. j , k >. , l >. ) <-> E. d e. A E. g e. A E. j e. A ( E. e e. B E. f e. C a = <. <. d , e >. , f >. /\ E. h e. B E. i e. C b = <. <. g , h >. , i >. /\ E. k e. B E. l e. C c = <. <. j , k >. , l >. ) )
33 3reeanv 
 |-  ( E. d e. A E. g e. A E. j e. A ( E. e e. B E. f e. C a = <. <. d , e >. , f >. /\ E. h e. B E. i e. C b = <. <. g , h >. , i >. /\ E. k e. B E. l e. C c = <. <. j , k >. , l >. ) <-> ( E. d e. A E. e e. B E. f e. C a = <. <. d , e >. , f >. /\ E. g e. A E. h e. B E. i e. C b = <. <. g , h >. , i >. /\ E. j e. A E. k e. B E. l e. C c = <. <. j , k >. , l >. ) )
34 32 33 bitri 
 |-  ( E. d e. A E. g e. A E. j e. A E. e e. B E. h e. B E. k e. B E. f e. C E. i e. C E. l e. C ( a = <. <. d , e >. , f >. /\ b = <. <. g , h >. , i >. /\ c = <. <. j , k >. , l >. ) <-> ( E. d e. A E. e e. B E. f e. C a = <. <. d , e >. , f >. /\ E. g e. A E. h e. B E. i e. C b = <. <. g , h >. , i >. /\ E. j e. A E. k e. B E. l e. C c = <. <. j , k >. , l >. ) )
35 25 34 bitr4i 
 |-  ( ( a e. ( ( A X. B ) X. C ) /\ b e. ( ( A X. B ) X. C ) /\ c e. ( ( A X. B ) X. C ) ) <-> E. d e. A E. g e. A E. j e. A E. e e. B E. h e. B E. k e. B E. f e. C E. i e. C E. l e. C ( a = <. <. d , e >. , f >. /\ b = <. <. g , h >. , i >. /\ c = <. <. j , k >. , l >. ) )
36 simprl1 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( d e. A /\ e e. B /\ f e. C ) )
37 simprr2 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( j e. A /\ k e. B /\ l e. C ) )
38 2 adantr 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> R Po A )
39 simpl11 
 |-  ( ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) -> d e. A )
40 39 adantl 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> d e. A )
41 simpr11 
 |-  ( ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) -> g e. A )
42 41 adantl 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> g e. A )
43 simpr21 
 |-  ( ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) -> j e. A )
44 43 adantl 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> j e. A )
45 potr 
 |-  ( ( R Po A /\ ( d e. A /\ g e. A /\ j e. A ) ) -> ( ( d R g /\ g R j ) -> d R j ) )
46 38 40 42 44 45 syl13anc 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( ( d R g /\ g R j ) -> d R j ) )
47 orc 
 |-  ( d R j -> ( d R j \/ d = j ) )
48 46 47 syl6 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( ( d R g /\ g R j ) -> ( d R j \/ d = j ) ) )
49 48 expd 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( d R g -> ( g R j -> ( d R j \/ d = j ) ) ) )
50 breq1 
 |-  ( d = g -> ( d R j <-> g R j ) )
51 50 47 syl6bir 
 |-  ( d = g -> ( g R j -> ( d R j \/ d = j ) ) )
52 51 a1i 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( d = g -> ( g R j -> ( d R j \/ d = j ) ) ) )
53 simp3l1 
 |-  ( ( ( 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 ) ) ) -> ( d R g \/ d = g ) )
54 53 ad2antrl 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( d R g \/ d = g ) )
55 49 52 54 mpjaod 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( g R j -> ( d R j \/ d = j ) ) )
56 breq2 
 |-  ( g = j -> ( d R g <-> d R j ) )
57 equequ2 
 |-  ( g = j -> ( d = g <-> d = j ) )
58 56 57 orbi12d 
 |-  ( g = j -> ( ( d R g \/ d = g ) <-> ( d R j \/ d = j ) ) )
59 54 58 syl5ibcom 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( g = j -> ( d R j \/ d = j ) ) )
60 simp3l1 
 |-  ( ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) -> ( g R j \/ g = j ) )
61 60 ad2antll 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( g R j \/ g = j ) )
62 55 59 61 mpjaod 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( d R j \/ d = j ) )
63 3 adantr 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> S Po B )
64 simpl12 
 |-  ( ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) -> e e. B )
65 64 adantl 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> e e. B )
66 simpr12 
 |-  ( ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) -> h e. B )
67 66 adantl 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> h e. B )
68 simpr22 
 |-  ( ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) -> k e. B )
69 68 adantl 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> k e. B )
70 potr 
 |-  ( ( S Po B /\ ( e e. B /\ h e. B /\ k e. B ) ) -> ( ( e S h /\ h S k ) -> e S k ) )
71 63 65 67 69 70 syl13anc 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( ( e S h /\ h S k ) -> e S k ) )
72 orc 
 |-  ( e S k -> ( e S k \/ e = k ) )
73 71 72 syl6 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( ( e S h /\ h S k ) -> ( e S k \/ e = k ) ) )
74 73 expd 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( e S h -> ( h S k -> ( e S k \/ e = k ) ) ) )
75 breq1 
 |-  ( e = h -> ( e S k <-> h S k ) )
76 75 72 syl6bir 
 |-  ( e = h -> ( h S k -> ( e S k \/ e = k ) ) )
77 76 a1i 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( e = h -> ( h S k -> ( e S k \/ e = k ) ) ) )
78 simp3l2 
 |-  ( ( ( 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 ) ) ) -> ( e S h \/ e = h ) )
79 78 ad2antrl 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( e S h \/ e = h ) )
80 74 77 79 mpjaod 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( h S k -> ( e S k \/ e = k ) ) )
81 breq2 
 |-  ( h = k -> ( e S h <-> e S k ) )
82 equequ2 
 |-  ( h = k -> ( e = h <-> e = k ) )
83 81 82 orbi12d 
 |-  ( h = k -> ( ( e S h \/ e = h ) <-> ( e S k \/ e = k ) ) )
84 79 83 syl5ibcom 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( h = k -> ( e S k \/ e = k ) ) )
85 simp3l2 
 |-  ( ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) -> ( h S k \/ h = k ) )
86 85 ad2antll 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( h S k \/ h = k ) )
87 80 84 86 mpjaod 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( e S k \/ e = k ) )
88 4 adantr 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> T Po C )
89 simpl13 
 |-  ( ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) -> f e. C )
90 89 adantl 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> f e. C )
91 simpr13 
 |-  ( ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) -> i e. C )
92 91 adantl 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> i e. C )
93 simpr23 
 |-  ( ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) -> l e. C )
94 93 adantl 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> l e. C )
95 potr 
 |-  ( ( T Po C /\ ( f e. C /\ i e. C /\ l e. C ) ) -> ( ( f T i /\ i T l ) -> f T l ) )
96 88 90 92 94 95 syl13anc 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( ( f T i /\ i T l ) -> f T l ) )
97 orc 
 |-  ( f T l -> ( f T l \/ f = l ) )
98 96 97 syl6 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( ( f T i /\ i T l ) -> ( f T l \/ f = l ) ) )
99 98 expd 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( f T i -> ( i T l -> ( f T l \/ f = l ) ) ) )
100 breq1 
 |-  ( f = i -> ( f T l <-> i T l ) )
101 100 97 syl6bir 
 |-  ( f = i -> ( i T l -> ( f T l \/ f = l ) ) )
102 101 a1i 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( f = i -> ( i T l -> ( f T l \/ f = l ) ) ) )
103 simp3l3 
 |-  ( ( ( 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 ) ) ) -> ( f T i \/ f = i ) )
104 103 ad2antrl 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( f T i \/ f = i ) )
105 99 102 104 mpjaod 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( i T l -> ( f T l \/ f = l ) ) )
106 breq2 
 |-  ( i = l -> ( f T i <-> f T l ) )
107 equequ2 
 |-  ( i = l -> ( f = i <-> f = l ) )
108 106 107 orbi12d 
 |-  ( i = l -> ( ( f T i \/ f = i ) <-> ( f T l \/ f = l ) ) )
109 104 108 syl5ibcom 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( i = l -> ( f T l \/ f = l ) ) )
110 simp3l3 
 |-  ( ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) -> ( i T l \/ i = l ) )
111 110 ad2antll 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( i T l \/ i = l ) )
112 105 109 111 mpjaod 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( f T l \/ f = l ) )
113 62 87 112 3jca 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( ( d R j \/ d = j ) /\ ( e S k \/ e = k ) /\ ( f T l \/ f = l ) ) )
114 simpr3r 
 |-  ( ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) -> ( g =/= j \/ h =/= k \/ i =/= l ) )
115 114 adantl 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( g =/= j \/ h =/= k \/ i =/= l ) )
116 df-ne 
 |-  ( g =/= j <-> -. g = j )
117 df-ne 
 |-  ( h =/= k <-> -. h = k )
118 df-ne 
 |-  ( i =/= l <-> -. i = l )
119 116 117 118 3orbi123i 
 |-  ( ( g =/= j \/ h =/= k \/ i =/= l ) <-> ( -. g = j \/ -. h = k \/ -. i = l ) )
120 3ianor 
 |-  ( -. ( g = j /\ h = k /\ i = l ) <-> ( -. g = j \/ -. h = k \/ -. i = l ) )
121 119 120 bitr4i 
 |-  ( ( g =/= j \/ h =/= k \/ i =/= l ) <-> -. ( g = j /\ h = k /\ i = l ) )
122 115 121 sylib 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> -. ( g = j /\ h = k /\ i = l ) )
123 df-ne 
 |-  ( d =/= j <-> -. d = j )
124 df-ne 
 |-  ( e =/= k <-> -. e = k )
125 df-ne 
 |-  ( f =/= l <-> -. f = l )
126 123 124 125 3orbi123i 
 |-  ( ( d =/= j \/ e =/= k \/ f =/= l ) <-> ( -. d = j \/ -. e = k \/ -. f = l ) )
127 3ianor 
 |-  ( -. ( d = j /\ e = k /\ f = l ) <-> ( -. d = j \/ -. e = k \/ -. f = l ) )
128 126 127 bitr4i 
 |-  ( ( d =/= j \/ e =/= k \/ f =/= l ) <-> -. ( d = j /\ e = k /\ f = l ) )
129 128 con2bii 
 |-  ( ( d = j /\ e = k /\ f = l ) <-> -. ( d =/= j \/ e =/= k \/ f =/= l ) )
130 breq1 
 |-  ( d = j -> ( d R g <-> j R g ) )
131 equequ1 
 |-  ( d = j -> ( d = g <-> j = g ) )
132 equcom 
 |-  ( j = g <-> g = j )
133 131 132 bitrdi 
 |-  ( d = j -> ( d = g <-> g = j ) )
134 130 133 orbi12d 
 |-  ( d = j -> ( ( d R g \/ d = g ) <-> ( j R g \/ g = j ) ) )
135 54 134 syl5ibcom 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( d = j -> ( j R g \/ g = j ) ) )
136 135 imp 
 |-  ( ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) /\ d = j ) -> ( j R g \/ g = j ) )
137 61 adantr 
 |-  ( ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) /\ d = j ) -> ( g R j \/ g = j ) )
138 ordir 
 |-  ( ( ( j R g /\ g R j ) \/ g = j ) <-> ( ( j R g \/ g = j ) /\ ( g R j \/ g = j ) ) )
139 136 137 138 sylanbrc 
 |-  ( ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) /\ d = j ) -> ( ( j R g /\ g R j ) \/ g = j ) )
140 po2nr 
 |-  ( ( R Po A /\ ( j e. A /\ g e. A ) ) -> -. ( j R g /\ g R j ) )
141 38 44 42 140 syl12anc 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> -. ( j R g /\ g R j ) )
142 141 adantr 
 |-  ( ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) /\ d = j ) -> -. ( j R g /\ g R j ) )
143 139 142 orcnd 
 |-  ( ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) /\ d = j ) -> g = j )
144 143 ex 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( d = j -> g = j ) )
145 breq1 
 |-  ( e = k -> ( e S h <-> k S h ) )
146 equequ1 
 |-  ( e = k -> ( e = h <-> k = h ) )
147 equcom 
 |-  ( k = h <-> h = k )
148 146 147 bitrdi 
 |-  ( e = k -> ( e = h <-> h = k ) )
149 145 148 orbi12d 
 |-  ( e = k -> ( ( e S h \/ e = h ) <-> ( k S h \/ h = k ) ) )
150 79 149 syl5ibcom 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( e = k -> ( k S h \/ h = k ) ) )
151 150 imp 
 |-  ( ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) /\ e = k ) -> ( k S h \/ h = k ) )
152 86 adantr 
 |-  ( ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) /\ e = k ) -> ( h S k \/ h = k ) )
153 ordir 
 |-  ( ( ( k S h /\ h S k ) \/ h = k ) <-> ( ( k S h \/ h = k ) /\ ( h S k \/ h = k ) ) )
154 151 152 153 sylanbrc 
 |-  ( ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) /\ e = k ) -> ( ( k S h /\ h S k ) \/ h = k ) )
155 po2nr 
 |-  ( ( S Po B /\ ( k e. B /\ h e. B ) ) -> -. ( k S h /\ h S k ) )
156 63 69 67 155 syl12anc 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> -. ( k S h /\ h S k ) )
157 156 adantr 
 |-  ( ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) /\ e = k ) -> -. ( k S h /\ h S k ) )
158 154 157 orcnd 
 |-  ( ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) /\ e = k ) -> h = k )
159 158 ex 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( e = k -> h = k ) )
160 breq1 
 |-  ( f = l -> ( f T i <-> l T i ) )
161 equequ1 
 |-  ( f = l -> ( f = i <-> l = i ) )
162 160 161 orbi12d 
 |-  ( f = l -> ( ( f T i \/ f = i ) <-> ( l T i \/ l = i ) ) )
163 104 162 syl5ibcom 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( f = l -> ( l T i \/ l = i ) ) )
164 163 imp 
 |-  ( ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) /\ f = l ) -> ( l T i \/ l = i ) )
165 equcom 
 |-  ( l = i <-> i = l )
166 165 orbi2i 
 |-  ( ( l T i \/ l = i ) <-> ( l T i \/ i = l ) )
167 164 166 sylib 
 |-  ( ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) /\ f = l ) -> ( l T i \/ i = l ) )
168 111 adantr 
 |-  ( ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) /\ f = l ) -> ( i T l \/ i = l ) )
169 ordir 
 |-  ( ( ( l T i /\ i T l ) \/ i = l ) <-> ( ( l T i \/ i = l ) /\ ( i T l \/ i = l ) ) )
170 167 168 169 sylanbrc 
 |-  ( ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) /\ f = l ) -> ( ( l T i /\ i T l ) \/ i = l ) )
171 po2nr 
 |-  ( ( T Po C /\ ( l e. C /\ i e. C ) ) -> -. ( l T i /\ i T l ) )
172 88 94 92 171 syl12anc 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> -. ( l T i /\ i T l ) )
173 172 adantr 
 |-  ( ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) /\ f = l ) -> -. ( l T i /\ i T l ) )
174 170 173 orcnd 
 |-  ( ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) /\ f = l ) -> i = l )
175 174 ex 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( f = l -> i = l ) )
176 144 159 175 3anim123d 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( ( d = j /\ e = k /\ f = l ) -> ( g = j /\ h = k /\ i = l ) ) )
177 129 176 syl5bir 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( -. ( d =/= j \/ e =/= k \/ f =/= l ) -> ( g = j /\ h = k /\ i = l ) ) )
178 122 177 mt3d 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( d =/= j \/ e =/= k \/ f =/= l ) )
179 113 178 jca 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( ( ( d R j \/ d = j ) /\ ( e S k \/ e = k ) /\ ( f T l \/ f = l ) ) /\ ( d =/= j \/ e =/= k \/ f =/= l ) ) )
180 36 37 179 3jca 
 |-  ( ( ph /\ ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) -> ( ( d e. A /\ e e. B /\ f e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( d R j \/ d = j ) /\ ( e S k \/ e = k ) /\ ( f T l \/ f = l ) ) /\ ( d =/= j \/ e =/= k \/ f =/= l ) ) ) )
181 180 ex 
 |-  ( ph -> ( ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) -> ( ( d e. A /\ e e. B /\ f e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( d R j \/ d = j ) /\ ( e S k \/ e = k ) /\ ( f T l \/ f = l ) ) /\ ( d =/= j \/ e =/= k \/ f =/= l ) ) ) ) )
182 breq12 
 |-  ( ( a = <. <. d , e >. , f >. /\ b = <. <. g , h >. , i >. ) -> ( a U b <-> <. <. d , e >. , f >. U <. <. g , h >. , i >. ) )
183 182 3adant3 
 |-  ( ( a = <. <. d , e >. , f >. /\ b = <. <. g , h >. , i >. /\ c = <. <. j , k >. , l >. ) -> ( a U b <-> <. <. d , e >. , f >. U <. <. g , h >. , i >. ) )
184 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 ) ) ) )
185 183 184 bitrdi 
 |-  ( ( a = <. <. d , e >. , f >. /\ b = <. <. g , h >. , i >. /\ c = <. <. j , k >. , l >. ) -> ( a U b <-> ( ( 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 ) ) ) ) )
186 breq12 
 |-  ( ( b = <. <. g , h >. , i >. /\ c = <. <. j , k >. , l >. ) -> ( b U c <-> <. <. g , h >. , i >. U <. <. j , k >. , l >. ) )
187 186 3adant1 
 |-  ( ( a = <. <. d , e >. , f >. /\ b = <. <. g , h >. , i >. /\ c = <. <. j , k >. , l >. ) -> ( b U c <-> <. <. g , h >. , i >. U <. <. j , k >. , l >. ) )
188 1 xpord3lem 
 |-  ( <. <. g , h >. , i >. U <. <. j , k >. , l >. <-> ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) )
189 187 188 bitrdi 
 |-  ( ( a = <. <. d , e >. , f >. /\ b = <. <. g , h >. , i >. /\ c = <. <. j , k >. , l >. ) -> ( b U c <-> ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) )
190 185 189 anbi12d 
 |-  ( ( a = <. <. d , e >. , f >. /\ b = <. <. g , h >. , i >. /\ c = <. <. j , k >. , l >. ) -> ( ( a U b /\ b U c ) <-> ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) ) )
191 breq12 
 |-  ( ( a = <. <. d , e >. , f >. /\ c = <. <. j , k >. , l >. ) -> ( a U c <-> <. <. d , e >. , f >. U <. <. j , k >. , l >. ) )
192 191 3adant2 
 |-  ( ( a = <. <. d , e >. , f >. /\ b = <. <. g , h >. , i >. /\ c = <. <. j , k >. , l >. ) -> ( a U c <-> <. <. d , e >. , f >. U <. <. j , k >. , l >. ) )
193 1 xpord3lem 
 |-  ( <. <. d , e >. , f >. U <. <. j , k >. , l >. <-> ( ( d e. A /\ e e. B /\ f e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( d R j \/ d = j ) /\ ( e S k \/ e = k ) /\ ( f T l \/ f = l ) ) /\ ( d =/= j \/ e =/= k \/ f =/= l ) ) ) )
194 192 193 bitrdi 
 |-  ( ( a = <. <. d , e >. , f >. /\ b = <. <. g , h >. , i >. /\ c = <. <. j , k >. , l >. ) -> ( a U c <-> ( ( d e. A /\ e e. B /\ f e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( d R j \/ d = j ) /\ ( e S k \/ e = k ) /\ ( f T l \/ f = l ) ) /\ ( d =/= j \/ e =/= k \/ f =/= l ) ) ) ) )
195 190 194 imbi12d 
 |-  ( ( a = <. <. d , e >. , f >. /\ b = <. <. g , h >. , i >. /\ c = <. <. j , k >. , l >. ) -> ( ( ( a U b /\ b U c ) -> a U c ) <-> ( ( ( ( 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 ) ) ) /\ ( ( g e. A /\ h e. B /\ i e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( g R j \/ g = j ) /\ ( h S k \/ h = k ) /\ ( i T l \/ i = l ) ) /\ ( g =/= j \/ h =/= k \/ i =/= l ) ) ) ) -> ( ( d e. A /\ e e. B /\ f e. C ) /\ ( j e. A /\ k e. B /\ l e. C ) /\ ( ( ( d R j \/ d = j ) /\ ( e S k \/ e = k ) /\ ( f T l \/ f = l ) ) /\ ( d =/= j \/ e =/= k \/ f =/= l ) ) ) ) ) )
196 181 195 syl5ibrcom 
 |-  ( ph -> ( ( a = <. <. d , e >. , f >. /\ b = <. <. g , h >. , i >. /\ c = <. <. j , k >. , l >. ) -> ( ( a U b /\ b U c ) -> a U c ) ) )
197 196 rexlimdvw 
 |-  ( ph -> ( E. l e. C ( a = <. <. d , e >. , f >. /\ b = <. <. g , h >. , i >. /\ c = <. <. j , k >. , l >. ) -> ( ( a U b /\ b U c ) -> a U c ) ) )
198 197 a1d 
 |-  ( ph -> ( ( f e. C /\ i e. C ) -> ( E. l e. C ( a = <. <. d , e >. , f >. /\ b = <. <. g , h >. , i >. /\ c = <. <. j , k >. , l >. ) -> ( ( a U b /\ b U c ) -> a U c ) ) ) )
199 198 rexlimdvv 
 |-  ( ph -> ( E. f e. C E. i e. C E. l e. C ( a = <. <. d , e >. , f >. /\ b = <. <. g , h >. , i >. /\ c = <. <. j , k >. , l >. ) -> ( ( a U b /\ b U c ) -> a U c ) ) )
200 199 rexlimdvw 
 |-  ( ph -> ( E. k e. B E. f e. C E. i e. C E. l e. C ( a = <. <. d , e >. , f >. /\ b = <. <. g , h >. , i >. /\ c = <. <. j , k >. , l >. ) -> ( ( a U b /\ b U c ) -> a U c ) ) )
201 200 a1d 
 |-  ( ph -> ( ( e e. B /\ h e. B ) -> ( E. k e. B E. f e. C E. i e. C E. l e. C ( a = <. <. d , e >. , f >. /\ b = <. <. g , h >. , i >. /\ c = <. <. j , k >. , l >. ) -> ( ( a U b /\ b U c ) -> a U c ) ) ) )
202 201 rexlimdvv 
 |-  ( ph -> ( E. e e. B E. h e. B E. k e. B E. f e. C E. i e. C E. l e. C ( a = <. <. d , e >. , f >. /\ b = <. <. g , h >. , i >. /\ c = <. <. j , k >. , l >. ) -> ( ( a U b /\ b U c ) -> a U c ) ) )
203 202 rexlimdvw 
 |-  ( ph -> ( E. j e. A E. e e. B E. h e. B E. k e. B E. f e. C E. i e. C E. l e. C ( a = <. <. d , e >. , f >. /\ b = <. <. g , h >. , i >. /\ c = <. <. j , k >. , l >. ) -> ( ( a U b /\ b U c ) -> a U c ) ) )
204 203 a1d 
 |-  ( ph -> ( ( d e. A /\ g e. A ) -> ( E. j e. A E. e e. B E. h e. B E. k e. B E. f e. C E. i e. C E. l e. C ( a = <. <. d , e >. , f >. /\ b = <. <. g , h >. , i >. /\ c = <. <. j , k >. , l >. ) -> ( ( a U b /\ b U c ) -> a U c ) ) ) )
205 204 rexlimdvv 
 |-  ( ph -> ( E. d e. A E. g e. A E. j e. A E. e e. B E. h e. B E. k e. B E. f e. C E. i e. C E. l e. C ( a = <. <. d , e >. , f >. /\ b = <. <. g , h >. , i >. /\ c = <. <. j , k >. , l >. ) -> ( ( a U b /\ b U c ) -> a U c ) ) )
206 35 205 syl5bi 
 |-  ( ph -> ( ( a e. ( ( A X. B ) X. C ) /\ b e. ( ( A X. B ) X. C ) /\ c e. ( ( A X. B ) X. C ) ) -> ( ( a U b /\ b U c ) -> a U c ) ) )
207 206 imp 
 |-  ( ( ph /\ ( a e. ( ( A X. B ) X. C ) /\ b e. ( ( A X. B ) X. C ) /\ c e. ( ( A X. B ) X. C ) ) ) -> ( ( a U b /\ b U c ) -> a U c ) )
208 22 207 ispod 
 |-  ( ph -> U Po ( ( A X. B ) X. C ) )