Metamath Proof Explorer

Theorem poxp2

Description: Another way of partially ordering a cross product of two classes. (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Hypotheses xpord2.1 
|- T = { <. x , y >. | ( x e. ( A X. B ) /\ y e. ( A X. B ) /\ ( ( ( 1st ` x ) R ( 1st ` y ) \/ ( 1st ` x ) = ( 1st ` y ) ) /\ ( ( 2nd ` x ) S ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) /\ x =/= y ) ) }
poxp2.1 
|- ( ph -> R Po A )
poxp2.2 
|- ( ph -> S Po B )
Assertion poxp2 
|- ( ph -> T Po ( A X. B ) )

Proof

Step Hyp Ref Expression
1 xpord2.1 
 |-  T = { <. x , y >. | ( x e. ( A X. B ) /\ y e. ( A X. B ) /\ ( ( ( 1st ` x ) R ( 1st ` y ) \/ ( 1st ` x ) = ( 1st ` y ) ) /\ ( ( 2nd ` x ) S ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) /\ x =/= y ) ) }
2 poxp2.1 
 |-  ( ph -> R Po A )
3 poxp2.2 
 |-  ( ph -> S Po B )
4 elxp2 
 |-  ( a e. ( A X. B ) <-> E. p e. A E. q e. B a = <. p , q >. )
5 equid 
 |-  p = p
6 equid 
 |-  q = q
7 5 6 pm3.2i 
 |-  ( p = p /\ q = q )
8 neorian 
 |-  ( ( p =/= p \/ q =/= q ) <-> -. ( p = p /\ q = q ) )
9 8 con2bii 
 |-  ( ( p = p /\ q = q ) <-> -. ( p =/= p \/ q =/= q ) )
10 7 9 mpbi 
 |-  -. ( p =/= p \/ q =/= q )
11 simp3 
 |-  ( ( ( p R p \/ p = p ) /\ ( q S q \/ q = q ) /\ ( p =/= p \/ q =/= q ) ) -> ( p =/= p \/ q =/= q ) )
12 10 11 mto 
 |-  -. ( ( p R p \/ p = p ) /\ ( q S q \/ q = q ) /\ ( p =/= p \/ q =/= q ) )
13 simp3 
 |-  ( ( ( p e. A /\ q e. B ) /\ ( p e. A /\ q e. B ) /\ ( ( p R p \/ p = p ) /\ ( q S q \/ q = q ) /\ ( p =/= p \/ q =/= q ) ) ) -> ( ( p R p \/ p = p ) /\ ( q S q \/ q = q ) /\ ( p =/= p \/ q =/= q ) ) )
14 12 13 mto 
 |-  -. ( ( p e. A /\ q e. B ) /\ ( p e. A /\ q e. B ) /\ ( ( p R p \/ p = p ) /\ ( q S q \/ q = q ) /\ ( p =/= p \/ q =/= q ) ) )
15 1 xpord2lem 
 |-  ( <. p , q >. T <. p , q >. <-> ( ( p e. A /\ q e. B ) /\ ( p e. A /\ q e. B ) /\ ( ( p R p \/ p = p ) /\ ( q S q \/ q = q ) /\ ( p =/= p \/ q =/= q ) ) ) )
16 14 15 mtbir 
 |-  -. <. p , q >. T <. p , q >.
17 breq12 
 |-  ( ( a = <. p , q >. /\ a = <. p , q >. ) -> ( a T a <-> <. p , q >. T <. p , q >. ) )
18 17 anidms 
 |-  ( a = <. p , q >. -> ( a T a <-> <. p , q >. T <. p , q >. ) )
19 16 18 mtbiri 
 |-  ( a = <. p , q >. -> -. a T a )
20 19 rexlimivw 
 |-  ( E. q e. B a = <. p , q >. -> -. a T a )
21 20 rexlimivw 
 |-  ( E. p e. A E. q e. B a = <. p , q >. -> -. a T a )
22 4 21 sylbi 
 |-  ( a e. ( A X. B ) -> -. a T a )
23 22 adantl 
 |-  ( ( ph /\ a e. ( A X. B ) ) -> -. a T a )
24 3reeanv 
 |-  ( E. p e. A E. r e. A E. t e. A ( E. q e. B a = <. p , q >. /\ E. s e. B b = <. r , s >. /\ E. u e. B c = <. t , u >. ) <-> ( E. p e. A E. q e. B a = <. p , q >. /\ E. r e. A E. s e. B b = <. r , s >. /\ E. t e. A E. u e. B c = <. t , u >. ) )
25 3reeanv 
 |-  ( E. q e. B E. s e. B E. u e. B ( a = <. p , q >. /\ b = <. r , s >. /\ c = <. t , u >. ) <-> ( E. q e. B a = <. p , q >. /\ E. s e. B b = <. r , s >. /\ E. u e. B c = <. t , u >. ) )
26 25 rexbii 
 |-  ( E. t e. A E. q e. B E. s e. B E. u e. B ( a = <. p , q >. /\ b = <. r , s >. /\ c = <. t , u >. ) <-> E. t e. A ( E. q e. B a = <. p , q >. /\ E. s e. B b = <. r , s >. /\ E. u e. B c = <. t , u >. ) )
27 26 2rexbii 
 |-  ( E. p e. A E. r e. A E. t e. A E. q e. B E. s e. B E. u e. B ( a = <. p , q >. /\ b = <. r , s >. /\ c = <. t , u >. ) <-> E. p e. A E. r e. A E. t e. A ( E. q e. B a = <. p , q >. /\ E. s e. B b = <. r , s >. /\ E. u e. B c = <. t , u >. ) )
28 elxp2 
 |-  ( b e. ( A X. B ) <-> E. r e. A E. s e. B b = <. r , s >. )
29 elxp2 
 |-  ( c e. ( A X. B ) <-> E. t e. A E. u e. B c = <. t , u >. )
30 4 28 29 3anbi123i 
 |-  ( ( a e. ( A X. B ) /\ b e. ( A X. B ) /\ c e. ( A X. B ) ) <-> ( E. p e. A E. q e. B a = <. p , q >. /\ E. r e. A E. s e. B b = <. r , s >. /\ E. t e. A E. u e. B c = <. t , u >. ) )
31 24 27 30 3bitr4ri 
 |-  ( ( a e. ( A X. B ) /\ b e. ( A X. B ) /\ c e. ( A X. B ) ) <-> E. p e. A E. r e. A E. t e. A E. q e. B E. s e. B E. u e. B ( a = <. p , q >. /\ b = <. r , s >. /\ c = <. t , u >. ) )
32 df-3an 
 |-  ( ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) <-> ( ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) ) /\ ( s e. B /\ u e. B ) ) )
33 simp3 
 |-  ( ( ( p e. A /\ q e. B ) /\ ( r e. A /\ s e. B ) /\ ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) ) -> ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) )
34 simp3 
 |-  ( ( ( r e. A /\ s e. B ) /\ ( t e. A /\ u e. B ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) -> ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) )
35 simpr1l 
 |-  ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) -> p e. A )
36 35 adantr 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> p e. A )
37 simpr2r 
 |-  ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) -> q e. B )
38 37 adantr 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> q e. B )
39 36 38 jca 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( p e. A /\ q e. B ) )
40 simpr2l 
 |-  ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) -> t e. A )
41 40 adantr 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> t e. A )
42 simpr3r 
 |-  ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) -> u e. B )
43 42 adantr 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> u e. B )
44 41 43 jca 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( t e. A /\ u e. B ) )
45 2 ad2antrr 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> R Po A )
46 simpr1r 
 |-  ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) -> r e. A )
47 46 adantr 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> r e. A )
48 potr 
 |-  ( ( R Po A /\ ( p e. A /\ r e. A /\ t e. A ) ) -> ( ( p R r /\ r R t ) -> p R t ) )
49 45 36 47 41 48 syl13anc 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( ( p R r /\ r R t ) -> p R t ) )
50 orc 
 |-  ( p R t -> ( p R t \/ p = t ) )
51 49 50 syl6 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( ( p R r /\ r R t ) -> ( p R t \/ p = t ) ) )
52 51 expd 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( p R r -> ( r R t -> ( p R t \/ p = t ) ) ) )
53 breq1 
 |-  ( p = r -> ( p R t <-> r R t ) )
54 53 50 syl6bir 
 |-  ( p = r -> ( r R t -> ( p R t \/ p = t ) ) )
55 54 a1i 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( p = r -> ( r R t -> ( p R t \/ p = t ) ) ) )
56 simprl1 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( p R r \/ p = r ) )
57 52 55 56 mpjaod 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( r R t -> ( p R t \/ p = t ) ) )
58 breq2 
 |-  ( r = t -> ( p R r <-> p R t ) )
59 equequ2 
 |-  ( r = t -> ( p = r <-> p = t ) )
60 58 59 orbi12d 
 |-  ( r = t -> ( ( p R r \/ p = r ) <-> ( p R t \/ p = t ) ) )
61 56 60 syl5ibcom 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( r = t -> ( p R t \/ p = t ) ) )
62 simprr1 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( r R t \/ r = t ) )
63 57 61 62 mpjaod 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( p R t \/ p = t ) )
64 3 ad2antrr 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> S Po B )
65 simpr3l 
 |-  ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) -> s e. B )
66 65 adantr 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> s e. B )
67 potr 
 |-  ( ( S Po B /\ ( q e. B /\ s e. B /\ u e. B ) ) -> ( ( q S s /\ s S u ) -> q S u ) )
68 64 38 66 43 67 syl13anc 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( ( q S s /\ s S u ) -> q S u ) )
69 orc 
 |-  ( q S u -> ( q S u \/ q = u ) )
70 68 69 syl6 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( ( q S s /\ s S u ) -> ( q S u \/ q = u ) ) )
71 70 expd 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( q S s -> ( s S u -> ( q S u \/ q = u ) ) ) )
72 breq1 
 |-  ( q = s -> ( q S u <-> s S u ) )
73 72 69 syl6bir 
 |-  ( q = s -> ( s S u -> ( q S u \/ q = u ) ) )
74 73 a1i 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( q = s -> ( s S u -> ( q S u \/ q = u ) ) ) )
75 simprl2 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( q S s \/ q = s ) )
76 71 74 75 mpjaod 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( s S u -> ( q S u \/ q = u ) ) )
77 breq2 
 |-  ( s = u -> ( q S s <-> q S u ) )
78 equequ2 
 |-  ( s = u -> ( q = s <-> q = u ) )
79 77 78 orbi12d 
 |-  ( s = u -> ( ( q S s \/ q = s ) <-> ( q S u \/ q = u ) ) )
80 75 79 syl5ibcom 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( s = u -> ( q S u \/ q = u ) ) )
81 simprr2 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( s S u \/ s = u ) )
82 76 80 81 mpjaod 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( q S u \/ q = u ) )
83 simprr3 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( r =/= t \/ s =/= u ) )
84 neorian 
 |-  ( ( r =/= t \/ s =/= u ) <-> -. ( r = t /\ s = u ) )
85 83 84 sylib 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> -. ( r = t /\ s = u ) )
86 neorian 
 |-  ( ( p =/= t \/ q =/= u ) <-> -. ( p = t /\ q = u ) )
87 86 con2bii 
 |-  ( ( p = t /\ q = u ) <-> -. ( p =/= t \/ q =/= u ) )
88 breq1 
 |-  ( p = t -> ( p R r <-> t R r ) )
89 equequ1 
 |-  ( p = t -> ( p = r <-> t = r ) )
90 88 89 orbi12d 
 |-  ( p = t -> ( ( p R r \/ p = r ) <-> ( t R r \/ t = r ) ) )
91 90 adantr 
 |-  ( ( p = t /\ q = u ) -> ( ( p R r \/ p = r ) <-> ( t R r \/ t = r ) ) )
92 breq1 
 |-  ( q = u -> ( q S s <-> u S s ) )
93 equequ1 
 |-  ( q = u -> ( q = s <-> u = s ) )
94 92 93 orbi12d 
 |-  ( q = u -> ( ( q S s \/ q = s ) <-> ( u S s \/ u = s ) ) )
95 94 adantl 
 |-  ( ( p = t /\ q = u ) -> ( ( q S s \/ q = s ) <-> ( u S s \/ u = s ) ) )
96 neeq1 
 |-  ( p = t -> ( p =/= r <-> t =/= r ) )
97 96 adantr 
 |-  ( ( p = t /\ q = u ) -> ( p =/= r <-> t =/= r ) )
98 neeq1 
 |-  ( q = u -> ( q =/= s <-> u =/= s ) )
99 98 adantl 
 |-  ( ( p = t /\ q = u ) -> ( q =/= s <-> u =/= s ) )
100 97 99 orbi12d 
 |-  ( ( p = t /\ q = u ) -> ( ( p =/= r \/ q =/= s ) <-> ( t =/= r \/ u =/= s ) ) )
101 91 95 100 3anbi123d 
 |-  ( ( p = t /\ q = u ) -> ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) <-> ( ( t R r \/ t = r ) /\ ( u S s \/ u = s ) /\ ( t =/= r \/ u =/= s ) ) ) )
102 101 anbi1d 
 |-  ( ( p = t /\ q = u ) -> ( ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) <-> ( ( ( t R r \/ t = r ) /\ ( u S s \/ u = s ) /\ ( t =/= r \/ u =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) )
103 102 anbi2d 
 |-  ( ( p = t /\ q = u ) -> ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) <-> ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( t R r \/ t = r ) /\ ( u S s \/ u = s ) /\ ( t =/= r \/ u =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) ) )
104 simprl1 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( t R r \/ t = r ) /\ ( u S s \/ u = s ) /\ ( t =/= r \/ u =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( t R r \/ t = r ) )
105 simprr1 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( t R r \/ t = r ) /\ ( u S s \/ u = s ) /\ ( t =/= r \/ u =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( r R t \/ r = t ) )
106 orcom 
 |-  ( ( ( t R r /\ r R t ) \/ r = t ) <-> ( r = t \/ ( t R r /\ r R t ) ) )
107 ordi 
 |-  ( ( r = t \/ ( t R r /\ r R t ) ) <-> ( ( r = t \/ t R r ) /\ ( r = t \/ r R t ) ) )
108 orcom 
 |-  ( ( r = t \/ t R r ) <-> ( t R r \/ r = t ) )
109 equcom 
 |-  ( r = t <-> t = r )
110 109 orbi2i 
 |-  ( ( t R r \/ r = t ) <-> ( t R r \/ t = r ) )
111 108 110 bitri 
 |-  ( ( r = t \/ t R r ) <-> ( t R r \/ t = r ) )
112 orcom 
 |-  ( ( r = t \/ r R t ) <-> ( r R t \/ r = t ) )
113 111 112 anbi12i 
 |-  ( ( ( r = t \/ t R r ) /\ ( r = t \/ r R t ) ) <-> ( ( t R r \/ t = r ) /\ ( r R t \/ r = t ) ) )
114 106 107 113 3bitri 
 |-  ( ( ( t R r /\ r R t ) \/ r = t ) <-> ( ( t R r \/ t = r ) /\ ( r R t \/ r = t ) ) )
115 104 105 114 sylanbrc 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( t R r \/ t = r ) /\ ( u S s \/ u = s ) /\ ( t =/= r \/ u =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( ( t R r /\ r R t ) \/ r = t ) )
116 2 ad2antrr 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( t R r \/ t = r ) /\ ( u S s \/ u = s ) /\ ( t =/= r \/ u =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> R Po A )
117 40 adantr 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( t R r \/ t = r ) /\ ( u S s \/ u = s ) /\ ( t =/= r \/ u =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> t e. A )
118 46 adantr 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( t R r \/ t = r ) /\ ( u S s \/ u = s ) /\ ( t =/= r \/ u =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> r e. A )
119 po2nr 
 |-  ( ( R Po A /\ ( t e. A /\ r e. A ) ) -> -. ( t R r /\ r R t ) )
120 116 117 118 119 syl12anc 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( t R r \/ t = r ) /\ ( u S s \/ u = s ) /\ ( t =/= r \/ u =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> -. ( t R r /\ r R t ) )
121 115 120 orcnd 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( t R r \/ t = r ) /\ ( u S s \/ u = s ) /\ ( t =/= r \/ u =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> r = t )
122 simprl2 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( t R r \/ t = r ) /\ ( u S s \/ u = s ) /\ ( t =/= r \/ u =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( u S s \/ u = s ) )
123 simprr2 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( t R r \/ t = r ) /\ ( u S s \/ u = s ) /\ ( t =/= r \/ u =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( s S u \/ s = u ) )
124 orcom 
 |-  ( ( ( u S s /\ s S u ) \/ s = u ) <-> ( s = u \/ ( u S s /\ s S u ) ) )
125 ordi 
 |-  ( ( s = u \/ ( u S s /\ s S u ) ) <-> ( ( s = u \/ u S s ) /\ ( s = u \/ s S u ) ) )
126 orcom 
 |-  ( ( s = u \/ u S s ) <-> ( u S s \/ s = u ) )
127 equcom 
 |-  ( s = u <-> u = s )
128 127 orbi2i 
 |-  ( ( u S s \/ s = u ) <-> ( u S s \/ u = s ) )
129 126 128 bitri 
 |-  ( ( s = u \/ u S s ) <-> ( u S s \/ u = s ) )
130 orcom 
 |-  ( ( s = u \/ s S u ) <-> ( s S u \/ s = u ) )
131 129 130 anbi12i 
 |-  ( ( ( s = u \/ u S s ) /\ ( s = u \/ s S u ) ) <-> ( ( u S s \/ u = s ) /\ ( s S u \/ s = u ) ) )
132 124 125 131 3bitri 
 |-  ( ( ( u S s /\ s S u ) \/ s = u ) <-> ( ( u S s \/ u = s ) /\ ( s S u \/ s = u ) ) )
133 122 123 132 sylanbrc 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( t R r \/ t = r ) /\ ( u S s \/ u = s ) /\ ( t =/= r \/ u =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( ( u S s /\ s S u ) \/ s = u ) )
134 3 ad2antrr 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( t R r \/ t = r ) /\ ( u S s \/ u = s ) /\ ( t =/= r \/ u =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> S Po B )
135 42 adantr 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( t R r \/ t = r ) /\ ( u S s \/ u = s ) /\ ( t =/= r \/ u =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> u e. B )
136 65 adantr 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( t R r \/ t = r ) /\ ( u S s \/ u = s ) /\ ( t =/= r \/ u =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> s e. B )
137 po2nr 
 |-  ( ( S Po B /\ ( u e. B /\ s e. B ) ) -> -. ( u S s /\ s S u ) )
138 134 135 136 137 syl12anc 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( t R r \/ t = r ) /\ ( u S s \/ u = s ) /\ ( t =/= r \/ u =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> -. ( u S s /\ s S u ) )
139 133 138 orcnd 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( t R r \/ t = r ) /\ ( u S s \/ u = s ) /\ ( t =/= r \/ u =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> s = u )
140 121 139 jca 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( t R r \/ t = r ) /\ ( u S s \/ u = s ) /\ ( t =/= r \/ u =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( r = t /\ s = u ) )
141 103 140 syl6bi 
 |-  ( ( p = t /\ q = u ) -> ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( r = t /\ s = u ) ) )
142 141 com12 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( ( p = t /\ q = u ) -> ( r = t /\ s = u ) ) )
143 87 142 syl5bir 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( -. ( p =/= t \/ q =/= u ) -> ( r = t /\ s = u ) ) )
144 85 143 mt3d 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( p =/= t \/ q =/= u ) )
145 63 82 144 3jca 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( ( p R t \/ p = t ) /\ ( q S u \/ q = u ) /\ ( p =/= t \/ q =/= u ) ) )
146 39 44 145 3jca 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) /\ ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( ( p e. A /\ q e. B ) /\ ( t e. A /\ u e. B ) /\ ( ( p R t \/ p = t ) /\ ( q S u \/ q = u ) /\ ( p =/= t \/ q =/= u ) ) ) )
147 146 ex 
 |-  ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) -> ( ( ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) -> ( ( p e. A /\ q e. B ) /\ ( t e. A /\ u e. B ) /\ ( ( p R t \/ p = t ) /\ ( q S u \/ q = u ) /\ ( p =/= t \/ q =/= u ) ) ) ) )
148 33 34 147 syl2ani 
 |-  ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) -> ( ( ( ( p e. A /\ q e. B ) /\ ( r e. A /\ s e. B ) /\ ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) ) /\ ( ( r e. A /\ s e. B ) /\ ( t e. A /\ u e. B ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( ( p e. A /\ q e. B ) /\ ( t e. A /\ u e. B ) /\ ( ( p R t \/ p = t ) /\ ( q S u \/ q = u ) /\ ( p =/= t \/ q =/= u ) ) ) ) )
149 breq12 
 |-  ( ( a = <. p , q >. /\ b = <. r , s >. ) -> ( a T b <-> <. p , q >. T <. r , s >. ) )
150 149 3adant3 
 |-  ( ( a = <. p , q >. /\ b = <. r , s >. /\ c = <. t , u >. ) -> ( a T b <-> <. p , q >. T <. r , s >. ) )
151 1 xpord2lem 
 |-  ( <. p , q >. T <. r , s >. <-> ( ( p e. A /\ q e. B ) /\ ( r e. A /\ s e. B ) /\ ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) ) )
152 150 151 bitrdi 
 |-  ( ( a = <. p , q >. /\ b = <. r , s >. /\ c = <. t , u >. ) -> ( a T b <-> ( ( p e. A /\ q e. B ) /\ ( r e. A /\ s e. B ) /\ ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) ) ) )
153 breq12 
 |-  ( ( b = <. r , s >. /\ c = <. t , u >. ) -> ( b T c <-> <. r , s >. T <. t , u >. ) )
154 153 3adant1 
 |-  ( ( a = <. p , q >. /\ b = <. r , s >. /\ c = <. t , u >. ) -> ( b T c <-> <. r , s >. T <. t , u >. ) )
155 1 xpord2lem 
 |-  ( <. r , s >. T <. t , u >. <-> ( ( r e. A /\ s e. B ) /\ ( t e. A /\ u e. B ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) )
156 154 155 bitrdi 
 |-  ( ( a = <. p , q >. /\ b = <. r , s >. /\ c = <. t , u >. ) -> ( b T c <-> ( ( r e. A /\ s e. B ) /\ ( t e. A /\ u e. B ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) )
157 152 156 anbi12d 
 |-  ( ( a = <. p , q >. /\ b = <. r , s >. /\ c = <. t , u >. ) -> ( ( a T b /\ b T c ) <-> ( ( ( p e. A /\ q e. B ) /\ ( r e. A /\ s e. B ) /\ ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) ) /\ ( ( r e. A /\ s e. B ) /\ ( t e. A /\ u e. B ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) ) )
158 breq12 
 |-  ( ( a = <. p , q >. /\ c = <. t , u >. ) -> ( a T c <-> <. p , q >. T <. t , u >. ) )
159 158 3adant2 
 |-  ( ( a = <. p , q >. /\ b = <. r , s >. /\ c = <. t , u >. ) -> ( a T c <-> <. p , q >. T <. t , u >. ) )
160 1 xpord2lem 
 |-  ( <. p , q >. T <. t , u >. <-> ( ( p e. A /\ q e. B ) /\ ( t e. A /\ u e. B ) /\ ( ( p R t \/ p = t ) /\ ( q S u \/ q = u ) /\ ( p =/= t \/ q =/= u ) ) ) )
161 159 160 bitrdi 
 |-  ( ( a = <. p , q >. /\ b = <. r , s >. /\ c = <. t , u >. ) -> ( a T c <-> ( ( p e. A /\ q e. B ) /\ ( t e. A /\ u e. B ) /\ ( ( p R t \/ p = t ) /\ ( q S u \/ q = u ) /\ ( p =/= t \/ q =/= u ) ) ) ) )
162 157 161 imbi12d 
 |-  ( ( a = <. p , q >. /\ b = <. r , s >. /\ c = <. t , u >. ) -> ( ( ( a T b /\ b T c ) -> a T c ) <-> ( ( ( ( p e. A /\ q e. B ) /\ ( r e. A /\ s e. B ) /\ ( ( p R r \/ p = r ) /\ ( q S s \/ q = s ) /\ ( p =/= r \/ q =/= s ) ) ) /\ ( ( r e. A /\ s e. B ) /\ ( t e. A /\ u e. B ) /\ ( ( r R t \/ r = t ) /\ ( s S u \/ s = u ) /\ ( r =/= t \/ s =/= u ) ) ) ) -> ( ( p e. A /\ q e. B ) /\ ( t e. A /\ u e. B ) /\ ( ( p R t \/ p = t ) /\ ( q S u \/ q = u ) /\ ( p =/= t \/ q =/= u ) ) ) ) ) )
163 148 162 syl5ibrcom 
 |-  ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) /\ ( s e. B /\ u e. B ) ) ) -> ( ( a = <. p , q >. /\ b = <. r , s >. /\ c = <. t , u >. ) -> ( ( a T b /\ b T c ) -> a T c ) ) )
164 32 163 sylan2br 
 |-  ( ( ph /\ ( ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) ) /\ ( s e. B /\ u e. B ) ) ) -> ( ( a = <. p , q >. /\ b = <. r , s >. /\ c = <. t , u >. ) -> ( ( a T b /\ b T c ) -> a T c ) ) )
165 164 anassrs 
 |-  ( ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) ) ) /\ ( s e. B /\ u e. B ) ) -> ( ( a = <. p , q >. /\ b = <. r , s >. /\ c = <. t , u >. ) -> ( ( a T b /\ b T c ) -> a T c ) ) )
166 165 rexlimdvva 
 |-  ( ( ph /\ ( ( p e. A /\ r e. A ) /\ ( t e. A /\ q e. B ) ) ) -> ( E. s e. B E. u e. B ( a = <. p , q >. /\ b = <. r , s >. /\ c = <. t , u >. ) -> ( ( a T b /\ b T c ) -> a T c ) ) )
167 166 anassrs 
 |-  ( ( ( ph /\ ( p e. A /\ r e. A ) ) /\ ( t e. A /\ q e. B ) ) -> ( E. s e. B E. u e. B ( a = <. p , q >. /\ b = <. r , s >. /\ c = <. t , u >. ) -> ( ( a T b /\ b T c ) -> a T c ) ) )
168 167 rexlimdvva 
 |-  ( ( ph /\ ( p e. A /\ r e. A ) ) -> ( E. t e. A E. q e. B E. s e. B E. u e. B ( a = <. p , q >. /\ b = <. r , s >. /\ c = <. t , u >. ) -> ( ( a T b /\ b T c ) -> a T c ) ) )
169 168 rexlimdvva 
 |-  ( ph -> ( E. p e. A E. r e. A E. t e. A E. q e. B E. s e. B E. u e. B ( a = <. p , q >. /\ b = <. r , s >. /\ c = <. t , u >. ) -> ( ( a T b /\ b T c ) -> a T c ) ) )
170 169 imp 
 |-  ( ( ph /\ E. p e. A E. r e. A E. t e. A E. q e. B E. s e. B E. u e. B ( a = <. p , q >. /\ b = <. r , s >. /\ c = <. t , u >. ) ) -> ( ( a T b /\ b T c ) -> a T c ) )
171 31 170 sylan2b 
 |-  ( ( ph /\ ( a e. ( A X. B ) /\ b e. ( A X. B ) /\ c e. ( A X. B ) ) ) -> ( ( a T b /\ b T c ) -> a T c ) )
172 23 171 ispod 
 |-  ( ph -> T Po ( A X. B ) )