Metamath Proof Explorer


Theorem poxp

Description: A lexicographical ordering of two posets. (Contributed by Scott Fenton, 16-Mar-2011) (Revised by Mario Carneiro, 7-Mar-2013)

Ref Expression
Hypothesis poxp.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 ) ) ) ) }
Assertion poxp
|- ( ( R Po A /\ S Po B ) -> T Po ( A X. B ) )

Proof

Step Hyp Ref Expression
1 poxp.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 ) ) ) ) }
2 elxp
 |-  ( t e. ( A X. B ) <-> E. a E. b ( t = <. a , b >. /\ ( a e. A /\ b e. B ) ) )
3 elxp
 |-  ( u e. ( A X. B ) <-> E. c E. d ( u = <. c , d >. /\ ( c e. A /\ d e. B ) ) )
4 elxp
 |-  ( v e. ( A X. B ) <-> E. e E. f ( v = <. e , f >. /\ ( e e. A /\ f e. B ) ) )
5 3an6
 |-  ( ( ( t = <. a , b >. /\ ( a e. A /\ b e. B ) ) /\ ( u = <. c , d >. /\ ( c e. A /\ d e. B ) ) /\ ( v = <. e , f >. /\ ( e e. A /\ f e. B ) ) ) <-> ( ( t = <. a , b >. /\ u = <. c , d >. /\ v = <. e , f >. ) /\ ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) /\ ( e e. A /\ f e. B ) ) ) )
6 poirr
 |-  ( ( R Po A /\ a e. A ) -> -. a R a )
7 6 ex
 |-  ( R Po A -> ( a e. A -> -. a R a ) )
8 poirr
 |-  ( ( S Po B /\ b e. B ) -> -. b S b )
9 8 intnand
 |-  ( ( S Po B /\ b e. B ) -> -. ( a = a /\ b S b ) )
10 9 ex
 |-  ( S Po B -> ( b e. B -> -. ( a = a /\ b S b ) ) )
11 7 10 im2anan9
 |-  ( ( R Po A /\ S Po B ) -> ( ( a e. A /\ b e. B ) -> ( -. a R a /\ -. ( a = a /\ b S b ) ) ) )
12 ioran
 |-  ( -. ( a R a \/ ( a = a /\ b S b ) ) <-> ( -. a R a /\ -. ( a = a /\ b S b ) ) )
13 11 12 syl6ibr
 |-  ( ( R Po A /\ S Po B ) -> ( ( a e. A /\ b e. B ) -> -. ( a R a \/ ( a = a /\ b S b ) ) ) )
14 13 imp
 |-  ( ( ( R Po A /\ S Po B ) /\ ( a e. A /\ b e. B ) ) -> -. ( a R a \/ ( a = a /\ b S b ) ) )
15 14 intnand
 |-  ( ( ( R Po A /\ S Po B ) /\ ( a e. A /\ b e. B ) ) -> -. ( ( ( a e. A /\ a e. A ) /\ ( b e. B /\ b e. B ) ) /\ ( a R a \/ ( a = a /\ b S b ) ) ) )
16 15 3ad2antr1
 |-  ( ( ( R Po A /\ S Po B ) /\ ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) /\ ( e e. A /\ f e. B ) ) ) -> -. ( ( ( a e. A /\ a e. A ) /\ ( b e. B /\ b e. B ) ) /\ ( a R a \/ ( a = a /\ b S b ) ) ) )
17 an4
 |-  ( ( ( ( ( a e. A /\ c e. A ) /\ ( b e. B /\ d e. B ) ) /\ ( a R c \/ ( a = c /\ b S d ) ) ) /\ ( ( ( c e. A /\ e e. A ) /\ ( d e. B /\ f e. B ) ) /\ ( c R e \/ ( c = e /\ d S f ) ) ) ) <-> ( ( ( ( a e. A /\ c e. A ) /\ ( b e. B /\ d e. B ) ) /\ ( ( c e. A /\ e e. A ) /\ ( d e. B /\ f e. B ) ) ) /\ ( ( a R c \/ ( a = c /\ b S d ) ) /\ ( c R e \/ ( c = e /\ d S f ) ) ) ) )
18 3an6
 |-  ( ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) /\ ( e e. A /\ f e. B ) ) <-> ( ( a e. A /\ c e. A /\ e e. A ) /\ ( b e. B /\ d e. B /\ f e. B ) ) )
19 potr
 |-  ( ( R Po A /\ ( a e. A /\ c e. A /\ e e. A ) ) -> ( ( a R c /\ c R e ) -> a R e ) )
20 19 3impia
 |-  ( ( R Po A /\ ( a e. A /\ c e. A /\ e e. A ) /\ ( a R c /\ c R e ) ) -> a R e )
21 20 orcd
 |-  ( ( R Po A /\ ( a e. A /\ c e. A /\ e e. A ) /\ ( a R c /\ c R e ) ) -> ( a R e \/ ( a = e /\ b S f ) ) )
22 21 3expia
 |-  ( ( R Po A /\ ( a e. A /\ c e. A /\ e e. A ) ) -> ( ( a R c /\ c R e ) -> ( a R e \/ ( a = e /\ b S f ) ) ) )
23 22 expdimp
 |-  ( ( ( R Po A /\ ( a e. A /\ c e. A /\ e e. A ) ) /\ a R c ) -> ( c R e -> ( a R e \/ ( a = e /\ b S f ) ) ) )
24 breq2
 |-  ( c = e -> ( a R c <-> a R e ) )
25 24 biimpa
 |-  ( ( c = e /\ a R c ) -> a R e )
26 25 orcd
 |-  ( ( c = e /\ a R c ) -> ( a R e \/ ( a = e /\ b S f ) ) )
27 26 expcom
 |-  ( a R c -> ( c = e -> ( a R e \/ ( a = e /\ b S f ) ) ) )
28 27 adantrd
 |-  ( a R c -> ( ( c = e /\ d S f ) -> ( a R e \/ ( a = e /\ b S f ) ) ) )
29 28 adantl
 |-  ( ( ( R Po A /\ ( a e. A /\ c e. A /\ e e. A ) ) /\ a R c ) -> ( ( c = e /\ d S f ) -> ( a R e \/ ( a = e /\ b S f ) ) ) )
30 23 29 jaod
 |-  ( ( ( R Po A /\ ( a e. A /\ c e. A /\ e e. A ) ) /\ a R c ) -> ( ( c R e \/ ( c = e /\ d S f ) ) -> ( a R e \/ ( a = e /\ b S f ) ) ) )
31 30 ex
 |-  ( ( R Po A /\ ( a e. A /\ c e. A /\ e e. A ) ) -> ( a R c -> ( ( c R e \/ ( c = e /\ d S f ) ) -> ( a R e \/ ( a = e /\ b S f ) ) ) ) )
32 potr
 |-  ( ( S Po B /\ ( b e. B /\ d e. B /\ f e. B ) ) -> ( ( b S d /\ d S f ) -> b S f ) )
33 32 expdimp
 |-  ( ( ( S Po B /\ ( b e. B /\ d e. B /\ f e. B ) ) /\ b S d ) -> ( d S f -> b S f ) )
34 33 anim2d
 |-  ( ( ( S Po B /\ ( b e. B /\ d e. B /\ f e. B ) ) /\ b S d ) -> ( ( c = e /\ d S f ) -> ( c = e /\ b S f ) ) )
35 34 orim2d
 |-  ( ( ( S Po B /\ ( b e. B /\ d e. B /\ f e. B ) ) /\ b S d ) -> ( ( c R e \/ ( c = e /\ d S f ) ) -> ( c R e \/ ( c = e /\ b S f ) ) ) )
36 breq1
 |-  ( a = c -> ( a R e <-> c R e ) )
37 equequ1
 |-  ( a = c -> ( a = e <-> c = e ) )
38 37 anbi1d
 |-  ( a = c -> ( ( a = e /\ b S f ) <-> ( c = e /\ b S f ) ) )
39 36 38 orbi12d
 |-  ( a = c -> ( ( a R e \/ ( a = e /\ b S f ) ) <-> ( c R e \/ ( c = e /\ b S f ) ) ) )
40 39 imbi2d
 |-  ( a = c -> ( ( ( c R e \/ ( c = e /\ d S f ) ) -> ( a R e \/ ( a = e /\ b S f ) ) ) <-> ( ( c R e \/ ( c = e /\ d S f ) ) -> ( c R e \/ ( c = e /\ b S f ) ) ) ) )
41 35 40 syl5ibr
 |-  ( a = c -> ( ( ( S Po B /\ ( b e. B /\ d e. B /\ f e. B ) ) /\ b S d ) -> ( ( c R e \/ ( c = e /\ d S f ) ) -> ( a R e \/ ( a = e /\ b S f ) ) ) ) )
42 41 expd
 |-  ( a = c -> ( ( S Po B /\ ( b e. B /\ d e. B /\ f e. B ) ) -> ( b S d -> ( ( c R e \/ ( c = e /\ d S f ) ) -> ( a R e \/ ( a = e /\ b S f ) ) ) ) ) )
43 42 com12
 |-  ( ( S Po B /\ ( b e. B /\ d e. B /\ f e. B ) ) -> ( a = c -> ( b S d -> ( ( c R e \/ ( c = e /\ d S f ) ) -> ( a R e \/ ( a = e /\ b S f ) ) ) ) ) )
44 43 impd
 |-  ( ( S Po B /\ ( b e. B /\ d e. B /\ f e. B ) ) -> ( ( a = c /\ b S d ) -> ( ( c R e \/ ( c = e /\ d S f ) ) -> ( a R e \/ ( a = e /\ b S f ) ) ) ) )
45 31 44 jaao
 |-  ( ( ( R Po A /\ ( a e. A /\ c e. A /\ e e. A ) ) /\ ( S Po B /\ ( b e. B /\ d e. B /\ f e. B ) ) ) -> ( ( a R c \/ ( a = c /\ b S d ) ) -> ( ( c R e \/ ( c = e /\ d S f ) ) -> ( a R e \/ ( a = e /\ b S f ) ) ) ) )
46 45 impd
 |-  ( ( ( R Po A /\ ( a e. A /\ c e. A /\ e e. A ) ) /\ ( S Po B /\ ( b e. B /\ d e. B /\ f e. B ) ) ) -> ( ( ( a R c \/ ( a = c /\ b S d ) ) /\ ( c R e \/ ( c = e /\ d S f ) ) ) -> ( a R e \/ ( a = e /\ b S f ) ) ) )
47 46 an4s
 |-  ( ( ( R Po A /\ S Po B ) /\ ( ( a e. A /\ c e. A /\ e e. A ) /\ ( b e. B /\ d e. B /\ f e. B ) ) ) -> ( ( ( a R c \/ ( a = c /\ b S d ) ) /\ ( c R e \/ ( c = e /\ d S f ) ) ) -> ( a R e \/ ( a = e /\ b S f ) ) ) )
48 18 47 sylan2b
 |-  ( ( ( R Po A /\ S Po B ) /\ ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) /\ ( e e. A /\ f e. B ) ) ) -> ( ( ( a R c \/ ( a = c /\ b S d ) ) /\ ( c R e \/ ( c = e /\ d S f ) ) ) -> ( a R e \/ ( a = e /\ b S f ) ) ) )
49 an4
 |-  ( ( ( a e. A /\ b e. B ) /\ ( e e. A /\ f e. B ) ) <-> ( ( a e. A /\ e e. A ) /\ ( b e. B /\ f e. B ) ) )
50 49 biimpi
 |-  ( ( ( a e. A /\ b e. B ) /\ ( e e. A /\ f e. B ) ) -> ( ( a e. A /\ e e. A ) /\ ( b e. B /\ f e. B ) ) )
51 50 3adant2
 |-  ( ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) /\ ( e e. A /\ f e. B ) ) -> ( ( a e. A /\ e e. A ) /\ ( b e. B /\ f e. B ) ) )
52 51 adantl
 |-  ( ( ( R Po A /\ S Po B ) /\ ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) /\ ( e e. A /\ f e. B ) ) ) -> ( ( a e. A /\ e e. A ) /\ ( b e. B /\ f e. B ) ) )
53 48 52 jctild
 |-  ( ( ( R Po A /\ S Po B ) /\ ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) /\ ( e e. A /\ f e. B ) ) ) -> ( ( ( a R c \/ ( a = c /\ b S d ) ) /\ ( c R e \/ ( c = e /\ d S f ) ) ) -> ( ( ( a e. A /\ e e. A ) /\ ( b e. B /\ f e. B ) ) /\ ( a R e \/ ( a = e /\ b S f ) ) ) ) )
54 53 adantld
 |-  ( ( ( R Po A /\ S Po B ) /\ ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) /\ ( e e. A /\ f e. B ) ) ) -> ( ( ( ( ( a e. A /\ c e. A ) /\ ( b e. B /\ d e. B ) ) /\ ( ( c e. A /\ e e. A ) /\ ( d e. B /\ f e. B ) ) ) /\ ( ( a R c \/ ( a = c /\ b S d ) ) /\ ( c R e \/ ( c = e /\ d S f ) ) ) ) -> ( ( ( a e. A /\ e e. A ) /\ ( b e. B /\ f e. B ) ) /\ ( a R e \/ ( a = e /\ b S f ) ) ) ) )
55 17 54 syl5bi
 |-  ( ( ( R Po A /\ S Po B ) /\ ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) /\ ( e e. A /\ f e. B ) ) ) -> ( ( ( ( ( a e. A /\ c e. A ) /\ ( b e. B /\ d e. B ) ) /\ ( a R c \/ ( a = c /\ b S d ) ) ) /\ ( ( ( c e. A /\ e e. A ) /\ ( d e. B /\ f e. B ) ) /\ ( c R e \/ ( c = e /\ d S f ) ) ) ) -> ( ( ( a e. A /\ e e. A ) /\ ( b e. B /\ f e. B ) ) /\ ( a R e \/ ( a = e /\ b S f ) ) ) ) )
56 16 55 jca
 |-  ( ( ( R Po A /\ S Po B ) /\ ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) /\ ( e e. A /\ f e. B ) ) ) -> ( -. ( ( ( a e. A /\ a e. A ) /\ ( b e. B /\ b e. B ) ) /\ ( a R a \/ ( a = a /\ b S b ) ) ) /\ ( ( ( ( ( a e. A /\ c e. A ) /\ ( b e. B /\ d e. B ) ) /\ ( a R c \/ ( a = c /\ b S d ) ) ) /\ ( ( ( c e. A /\ e e. A ) /\ ( d e. B /\ f e. B ) ) /\ ( c R e \/ ( c = e /\ d S f ) ) ) ) -> ( ( ( a e. A /\ e e. A ) /\ ( b e. B /\ f e. B ) ) /\ ( a R e \/ ( a = e /\ b S f ) ) ) ) ) )
57 breq12
 |-  ( ( t = <. a , b >. /\ t = <. a , b >. ) -> ( t T t <-> <. a , b >. T <. a , b >. ) )
58 57 anidms
 |-  ( t = <. a , b >. -> ( t T t <-> <. a , b >. T <. a , b >. ) )
59 58 notbid
 |-  ( t = <. a , b >. -> ( -. t T t <-> -. <. a , b >. T <. a , b >. ) )
60 59 3ad2ant1
 |-  ( ( t = <. a , b >. /\ u = <. c , d >. /\ v = <. e , f >. ) -> ( -. t T t <-> -. <. a , b >. T <. a , b >. ) )
61 breq12
 |-  ( ( t = <. a , b >. /\ u = <. c , d >. ) -> ( t T u <-> <. a , b >. T <. c , d >. ) )
62 61 3adant3
 |-  ( ( t = <. a , b >. /\ u = <. c , d >. /\ v = <. e , f >. ) -> ( t T u <-> <. a , b >. T <. c , d >. ) )
63 breq12
 |-  ( ( u = <. c , d >. /\ v = <. e , f >. ) -> ( u T v <-> <. c , d >. T <. e , f >. ) )
64 63 3adant1
 |-  ( ( t = <. a , b >. /\ u = <. c , d >. /\ v = <. e , f >. ) -> ( u T v <-> <. c , d >. T <. e , f >. ) )
65 62 64 anbi12d
 |-  ( ( t = <. a , b >. /\ u = <. c , d >. /\ v = <. e , f >. ) -> ( ( t T u /\ u T v ) <-> ( <. a , b >. T <. c , d >. /\ <. c , d >. T <. e , f >. ) ) )
66 breq12
 |-  ( ( t = <. a , b >. /\ v = <. e , f >. ) -> ( t T v <-> <. a , b >. T <. e , f >. ) )
67 66 3adant2
 |-  ( ( t = <. a , b >. /\ u = <. c , d >. /\ v = <. e , f >. ) -> ( t T v <-> <. a , b >. T <. e , f >. ) )
68 65 67 imbi12d
 |-  ( ( t = <. a , b >. /\ u = <. c , d >. /\ v = <. e , f >. ) -> ( ( ( t T u /\ u T v ) -> t T v ) <-> ( ( <. a , b >. T <. c , d >. /\ <. c , d >. T <. e , f >. ) -> <. a , b >. T <. e , f >. ) ) )
69 60 68 anbi12d
 |-  ( ( t = <. a , b >. /\ u = <. c , d >. /\ v = <. e , f >. ) -> ( ( -. t T t /\ ( ( t T u /\ u T v ) -> t T v ) ) <-> ( -. <. a , b >. T <. a , b >. /\ ( ( <. a , b >. T <. c , d >. /\ <. c , d >. T <. e , f >. ) -> <. a , b >. T <. e , f >. ) ) ) )
70 1 xporderlem
 |-  ( <. a , b >. T <. a , b >. <-> ( ( ( a e. A /\ a e. A ) /\ ( b e. B /\ b e. B ) ) /\ ( a R a \/ ( a = a /\ b S b ) ) ) )
71 70 notbii
 |-  ( -. <. a , b >. T <. a , b >. <-> -. ( ( ( a e. A /\ a e. A ) /\ ( b e. B /\ b e. B ) ) /\ ( a R a \/ ( a = a /\ b S b ) ) ) )
72 1 xporderlem
 |-  ( <. a , b >. T <. c , d >. <-> ( ( ( a e. A /\ c e. A ) /\ ( b e. B /\ d e. B ) ) /\ ( a R c \/ ( a = c /\ b S d ) ) ) )
73 1 xporderlem
 |-  ( <. c , d >. T <. e , f >. <-> ( ( ( c e. A /\ e e. A ) /\ ( d e. B /\ f e. B ) ) /\ ( c R e \/ ( c = e /\ d S f ) ) ) )
74 72 73 anbi12i
 |-  ( ( <. a , b >. T <. c , d >. /\ <. c , d >. T <. e , f >. ) <-> ( ( ( ( a e. A /\ c e. A ) /\ ( b e. B /\ d e. B ) ) /\ ( a R c \/ ( a = c /\ b S d ) ) ) /\ ( ( ( c e. A /\ e e. A ) /\ ( d e. B /\ f e. B ) ) /\ ( c R e \/ ( c = e /\ d S f ) ) ) ) )
75 1 xporderlem
 |-  ( <. a , b >. T <. e , f >. <-> ( ( ( a e. A /\ e e. A ) /\ ( b e. B /\ f e. B ) ) /\ ( a R e \/ ( a = e /\ b S f ) ) ) )
76 74 75 imbi12i
 |-  ( ( ( <. a , b >. T <. c , d >. /\ <. c , d >. T <. e , f >. ) -> <. a , b >. T <. e , f >. ) <-> ( ( ( ( ( a e. A /\ c e. A ) /\ ( b e. B /\ d e. B ) ) /\ ( a R c \/ ( a = c /\ b S d ) ) ) /\ ( ( ( c e. A /\ e e. A ) /\ ( d e. B /\ f e. B ) ) /\ ( c R e \/ ( c = e /\ d S f ) ) ) ) -> ( ( ( a e. A /\ e e. A ) /\ ( b e. B /\ f e. B ) ) /\ ( a R e \/ ( a = e /\ b S f ) ) ) ) )
77 71 76 anbi12i
 |-  ( ( -. <. a , b >. T <. a , b >. /\ ( ( <. a , b >. T <. c , d >. /\ <. c , d >. T <. e , f >. ) -> <. a , b >. T <. e , f >. ) ) <-> ( -. ( ( ( a e. A /\ a e. A ) /\ ( b e. B /\ b e. B ) ) /\ ( a R a \/ ( a = a /\ b S b ) ) ) /\ ( ( ( ( ( a e. A /\ c e. A ) /\ ( b e. B /\ d e. B ) ) /\ ( a R c \/ ( a = c /\ b S d ) ) ) /\ ( ( ( c e. A /\ e e. A ) /\ ( d e. B /\ f e. B ) ) /\ ( c R e \/ ( c = e /\ d S f ) ) ) ) -> ( ( ( a e. A /\ e e. A ) /\ ( b e. B /\ f e. B ) ) /\ ( a R e \/ ( a = e /\ b S f ) ) ) ) ) )
78 69 77 bitrdi
 |-  ( ( t = <. a , b >. /\ u = <. c , d >. /\ v = <. e , f >. ) -> ( ( -. t T t /\ ( ( t T u /\ u T v ) -> t T v ) ) <-> ( -. ( ( ( a e. A /\ a e. A ) /\ ( b e. B /\ b e. B ) ) /\ ( a R a \/ ( a = a /\ b S b ) ) ) /\ ( ( ( ( ( a e. A /\ c e. A ) /\ ( b e. B /\ d e. B ) ) /\ ( a R c \/ ( a = c /\ b S d ) ) ) /\ ( ( ( c e. A /\ e e. A ) /\ ( d e. B /\ f e. B ) ) /\ ( c R e \/ ( c = e /\ d S f ) ) ) ) -> ( ( ( a e. A /\ e e. A ) /\ ( b e. B /\ f e. B ) ) /\ ( a R e \/ ( a = e /\ b S f ) ) ) ) ) ) )
79 56 78 syl5ibr
 |-  ( ( t = <. a , b >. /\ u = <. c , d >. /\ v = <. e , f >. ) -> ( ( ( R Po A /\ S Po B ) /\ ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) /\ ( e e. A /\ f e. B ) ) ) -> ( -. t T t /\ ( ( t T u /\ u T v ) -> t T v ) ) ) )
80 79 expcomd
 |-  ( ( t = <. a , b >. /\ u = <. c , d >. /\ v = <. e , f >. ) -> ( ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) /\ ( e e. A /\ f e. B ) ) -> ( ( R Po A /\ S Po B ) -> ( -. t T t /\ ( ( t T u /\ u T v ) -> t T v ) ) ) ) )
81 80 imp
 |-  ( ( ( t = <. a , b >. /\ u = <. c , d >. /\ v = <. e , f >. ) /\ ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) /\ ( e e. A /\ f e. B ) ) ) -> ( ( R Po A /\ S Po B ) -> ( -. t T t /\ ( ( t T u /\ u T v ) -> t T v ) ) ) )
82 5 81 sylbi
 |-  ( ( ( t = <. a , b >. /\ ( a e. A /\ b e. B ) ) /\ ( u = <. c , d >. /\ ( c e. A /\ d e. B ) ) /\ ( v = <. e , f >. /\ ( e e. A /\ f e. B ) ) ) -> ( ( R Po A /\ S Po B ) -> ( -. t T t /\ ( ( t T u /\ u T v ) -> t T v ) ) ) )
83 82 3exp
 |-  ( ( t = <. a , b >. /\ ( a e. A /\ b e. B ) ) -> ( ( u = <. c , d >. /\ ( c e. A /\ d e. B ) ) -> ( ( v = <. e , f >. /\ ( e e. A /\ f e. B ) ) -> ( ( R Po A /\ S Po B ) -> ( -. t T t /\ ( ( t T u /\ u T v ) -> t T v ) ) ) ) ) )
84 83 com3l
 |-  ( ( u = <. c , d >. /\ ( c e. A /\ d e. B ) ) -> ( ( v = <. e , f >. /\ ( e e. A /\ f e. B ) ) -> ( ( t = <. a , b >. /\ ( a e. A /\ b e. B ) ) -> ( ( R Po A /\ S Po B ) -> ( -. t T t /\ ( ( t T u /\ u T v ) -> t T v ) ) ) ) ) )
85 84 exlimivv
 |-  ( E. c E. d ( u = <. c , d >. /\ ( c e. A /\ d e. B ) ) -> ( ( v = <. e , f >. /\ ( e e. A /\ f e. B ) ) -> ( ( t = <. a , b >. /\ ( a e. A /\ b e. B ) ) -> ( ( R Po A /\ S Po B ) -> ( -. t T t /\ ( ( t T u /\ u T v ) -> t T v ) ) ) ) ) )
86 85 com3l
 |-  ( ( v = <. e , f >. /\ ( e e. A /\ f e. B ) ) -> ( ( t = <. a , b >. /\ ( a e. A /\ b e. B ) ) -> ( E. c E. d ( u = <. c , d >. /\ ( c e. A /\ d e. B ) ) -> ( ( R Po A /\ S Po B ) -> ( -. t T t /\ ( ( t T u /\ u T v ) -> t T v ) ) ) ) ) )
87 86 exlimivv
 |-  ( E. e E. f ( v = <. e , f >. /\ ( e e. A /\ f e. B ) ) -> ( ( t = <. a , b >. /\ ( a e. A /\ b e. B ) ) -> ( E. c E. d ( u = <. c , d >. /\ ( c e. A /\ d e. B ) ) -> ( ( R Po A /\ S Po B ) -> ( -. t T t /\ ( ( t T u /\ u T v ) -> t T v ) ) ) ) ) )
88 87 com3l
 |-  ( ( t = <. a , b >. /\ ( a e. A /\ b e. B ) ) -> ( E. c E. d ( u = <. c , d >. /\ ( c e. A /\ d e. B ) ) -> ( E. e E. f ( v = <. e , f >. /\ ( e e. A /\ f e. B ) ) -> ( ( R Po A /\ S Po B ) -> ( -. t T t /\ ( ( t T u /\ u T v ) -> t T v ) ) ) ) ) )
89 88 exlimivv
 |-  ( E. a E. b ( t = <. a , b >. /\ ( a e. A /\ b e. B ) ) -> ( E. c E. d ( u = <. c , d >. /\ ( c e. A /\ d e. B ) ) -> ( E. e E. f ( v = <. e , f >. /\ ( e e. A /\ f e. B ) ) -> ( ( R Po A /\ S Po B ) -> ( -. t T t /\ ( ( t T u /\ u T v ) -> t T v ) ) ) ) ) )
90 89 3imp
 |-  ( ( E. a E. b ( t = <. a , b >. /\ ( a e. A /\ b e. B ) ) /\ E. c E. d ( u = <. c , d >. /\ ( c e. A /\ d e. B ) ) /\ E. e E. f ( v = <. e , f >. /\ ( e e. A /\ f e. B ) ) ) -> ( ( R Po A /\ S Po B ) -> ( -. t T t /\ ( ( t T u /\ u T v ) -> t T v ) ) ) )
91 2 3 4 90 syl3anb
 |-  ( ( t e. ( A X. B ) /\ u e. ( A X. B ) /\ v e. ( A X. B ) ) -> ( ( R Po A /\ S Po B ) -> ( -. t T t /\ ( ( t T u /\ u T v ) -> t T v ) ) ) )
92 91 3expia
 |-  ( ( t e. ( A X. B ) /\ u e. ( A X. B ) ) -> ( v e. ( A X. B ) -> ( ( R Po A /\ S Po B ) -> ( -. t T t /\ ( ( t T u /\ u T v ) -> t T v ) ) ) ) )
93 92 com3r
 |-  ( ( R Po A /\ S Po B ) -> ( ( t e. ( A X. B ) /\ u e. ( A X. B ) ) -> ( v e. ( A X. B ) -> ( -. t T t /\ ( ( t T u /\ u T v ) -> t T v ) ) ) ) )
94 93 imp
 |-  ( ( ( R Po A /\ S Po B ) /\ ( t e. ( A X. B ) /\ u e. ( A X. B ) ) ) -> ( v e. ( A X. B ) -> ( -. t T t /\ ( ( t T u /\ u T v ) -> t T v ) ) ) )
95 94 ralrimiv
 |-  ( ( ( R Po A /\ S Po B ) /\ ( t e. ( A X. B ) /\ u e. ( A X. B ) ) ) -> A. v e. ( A X. B ) ( -. t T t /\ ( ( t T u /\ u T v ) -> t T v ) ) )
96 95 ralrimivva
 |-  ( ( R Po A /\ S Po B ) -> A. t e. ( A X. B ) A. u e. ( A X. B ) A. v e. ( A X. B ) ( -. t T t /\ ( ( t T u /\ u T v ) -> t T v ) ) )
97 df-po
 |-  ( T Po ( A X. B ) <-> A. t e. ( A X. B ) A. u e. ( A X. B ) A. v e. ( A X. B ) ( -. t T t /\ ( ( t T u /\ u T v ) -> t T v ) ) )
98 96 97 sylibr
 |-  ( ( R Po A /\ S Po B ) -> T Po ( A X. B ) )