Theorem poxp 5794

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

Hypothesis

Ref	Expression
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

Ref	Expression
poxp	|- (( R Po A /\ S Po B) -> T Po (A X. B))

Distinct variable groups:   x,A,y   x,B,y   x, R,y   x, S,y

Allowed substitution hints:   T(x,y)

Proof of Theorem poxp

Dummy variables a b c d e f t u v are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elxp 4305	. . . . . . . 8 |- ( t e. (A X. B) <-> E. aE. b( t = <. a , b >. /\ ( a e. A /\ b e. B)))
2		elxp 4305	. . . . . . . 8 |- (u e. (A X. B) <-> E. cE. d(u = <. c , d >. /\ ( c e. A /\ d e. B)))
3		elxp 4305	. . . . . . . 8 |- (v e. (A X. B) <-> E. eE.f(v = <. e , f >. /\ ( e e. A /\ f e. B)))
4		3an6 1216	. . . . . . . . . . . . . . . . 17 |- ((( 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))))
5		poirr 4035	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (( R Po A /\ a e. A) -> -. a R a)
6	5	ex 108	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( R Po A -> ( a e. A -> -. a R a))
7		poirr 4035	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (( S Po B /\ b e. B) -> -. b S b)
8	7	intnand 839	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (( S Po B /\ b e. B) -> -. ( a = a /\ b S b))
9	8	ex 108	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( S Po B -> ( b e. B -> -. ( a = a /\ b S b)))
10	6, 9	im2anan9 530	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (( R Po A /\ S Po B) -> (( a e. A /\ b e. B) -> (-. a R a /\ -. ( a = a /\ b S b))))
11		ioran 668	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (-. ( a R a \/ ( a = a /\ b S b)) <-> (-. a R a /\ -. ( a = a /\ b S b)))
12	10, 11	syl6ibr 151	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (( R Po A /\ S Po B) -> (( a e. A /\ b e. B) -> -. ( a R a \/ ( a = a /\ b S b))))
13	12	imp 115	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((( R Po A /\ S Po B) /\ ( a e. A /\ b e. B)) -> -. ( a R a \/ ( a = a /\ b S b)))
14	13	intnand 839	. . . . . . . . . . . . . . . . . . . . . 22 |- ((( 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))))
15	14	3ad2antr1 1068	. . . . . . . . . . . . . . . . . . . . 21 |- ((( 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))))
16		an4 520	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((( 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 Sf)))) <-> (((( 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 Sf)))))
17		3an6 1216	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((( 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)))
18		potr 4036	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (( R Po A /\ ( a e. A /\ c e. A /\ e e. A)) -> (( a R c /\ c R e) -> a R e))
19	18	3impia 1100	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (( R Po A /\ ( a e. A /\ c e. A /\ e e. A) /\ ( a R c /\ c R e)) -> a R e)
20	19	orcd 651	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (( R Po A /\ ( a e. A /\ c e. A /\ e e. A) /\ ( a R c /\ c R e)) -> ( a R e \/ ( a = e /\ b Sf)))
21	20	3expia 1105	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (( R Po A /\ ( a e. A /\ c e. A /\ e e. A)) -> (( a R c /\ c R e) -> ( a R e \/ ( a = e /\ b Sf))))
22	21	expdimp 246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((( R Po A /\ ( a e. A /\ c e. A /\ e e. A)) /\ a R c) -> ( c R e -> ( a R e \/ ( a = e /\ b Sf))))
23		breq2 3759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( c = e -> ( a R c <-> a R e))
24	23	biimpa 280	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (( c = e /\ a R c) -> a R e)
25	24	orcd 651	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (( c = e /\ a R c) -> ( a R e \/ ( a = e /\ b Sf)))
26	25	expcom 109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( a R c -> ( c = e -> ( a R e \/ ( a = e /\ b Sf))))
27	26	adantrd 264	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( a R c -> (( c = e /\ d Sf) -> ( a R e \/ ( a = e /\ b Sf))))
28	27	adantl 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((( R Po A /\ ( a e. A /\ c e. A /\ e e. A)) /\ a R c) -> (( c = e /\ d Sf) -> ( a R e \/ ( a = e /\ b Sf))))
29	22, 28	jaod 636	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((( R Po A /\ ( a e. A /\ c e. A /\ e e. A)) /\ a R c) -> (( c R e \/ ( c = e /\ d Sf)) -> ( a R e \/ ( a = e /\ b Sf))))
30	29	ex 108	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (( R Po A /\ ( a e. A /\ c e. A /\ e e. A)) -> ( a R c -> (( c R e \/ ( c = e /\ d Sf)) -> ( a R e \/ ( a = e /\ b Sf)))))
31		potr 4036	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (( S Po B /\ ( b e. B /\ d e. B /\ f e. B)) -> (( b S d /\ d Sf) -> b Sf))
32	31	expdimp 246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((( S Po B /\ ( b e. B /\ d e. B /\ f e. B)) /\ b S d) -> ( d Sf -> b Sf))
33	32	anim2d 320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((( S Po B /\ ( b e. B /\ d e. B /\ f e. B)) /\ b S d) -> (( c = e /\ d Sf) -> ( c = e /\ b Sf)))
34	33	orim2d 701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((( S Po B /\ ( b e. B /\ d e. B /\ f e. B)) /\ b S d) -> (( c R e \/ ( c = e /\ d Sf)) -> ( c R e \/ ( c = e /\ b Sf))))
35		breq1 3758	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( a = c -> ( a R e <-> c R e))
36		equequ1 1595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( a = c -> ( a = e <-> c = e))
37	36	anbi1d 438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( a = c -> (( a = e /\ b Sf) <-> ( c = e /\ b Sf)))
38	35, 37	orbi12d 706	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( a = c -> (( a R e \/ ( a = e /\ b Sf)) <-> ( c R e \/ ( c = e /\ b Sf))))
39	38	imbi2d 219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( a = c -> ((( c R e \/ ( c = e /\ d Sf)) -> ( a R e \/ ( a = e /\ b Sf))) <-> (( c R e \/ ( c = e /\ d Sf)) -> ( c R e \/ ( c = e /\ b Sf)))))
40	34, 39	syl5ibr 145	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( a = c -> ((( S Po B /\ ( b e. B /\ d e. B /\ f e. B)) /\ b S d) -> (( c R e \/ ( c = e /\ d Sf)) -> ( a R e \/ ( a = e /\ b Sf)))))
41	40	expd 245	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( a = c -> (( S Po B /\ ( b e. B /\ d e. B /\ f e. B)) -> ( b S d -> (( c R e \/ ( c = e /\ d Sf)) -> ( a R e \/ ( a = e /\ b Sf))))))
42	41	com12 27	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (( S Po B /\ ( b e. B /\ d e. B /\ f e. B)) -> ( a = c -> ( b S d -> (( c R e \/ ( c = e /\ d Sf)) -> ( a R e \/ ( a = e /\ b Sf))))))
43	42	impd 242	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (( S Po B /\ ( b e. B /\ d e. B /\ f e. B)) -> (( a = c /\ b S d) -> (( c R e \/ ( c = e /\ d Sf)) -> ( a R e \/ ( a = e /\ b Sf)))))
44	30, 43	jaao 638	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((( 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 Sf)) -> ( a R e \/ ( a = e /\ b Sf)))))
45	44	impd 242	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((( 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 Sf))) -> ( a R e \/ ( a = e /\ b Sf))))
46	45	an4s 522	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((( 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 Sf))) -> ( a R e \/ ( a = e /\ b Sf))))
47	17, 46	sylan2b 271	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((( 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 Sf))) -> ( a R e \/ ( a = e /\ b Sf))))
48		an4 520	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((( a e. A /\ b e. B) /\ ( e e. A /\ f e. B)) <-> (( a e. A /\ e e. A) /\ ( b e. B /\ f e. B)))
49	48	biimpi 113	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((( 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	3adant2 922	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((( 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)))
51	50	adantl 262	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((( 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)))
52	47, 51	jctild 299	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((( 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 Sf))) -> ((( a e. A /\ e e. A) /\ ( b e. B /\ f e. B)) /\ ( a R e \/ ( a = e /\ b Sf)))))
53	52	adantld 263	. . . . . . . . . . . . . . . . . . . . . 22 |- ((( 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 Sf)))) -> ((( a e. A /\ e e. A) /\ ( b e. B /\ f e. B)) /\ ( a R e \/ ( a = e /\ b Sf)))))
54	16, 53	syl5bi 141	. . . . . . . . . . . . . . . . . . . . 21 |- ((( 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 Sf)))) -> ((( a e. A /\ e e. A) /\ ( b e. B /\ f e. B)) /\ ( a R e \/ ( a = e /\ b Sf)))))
55	15, 54	jca 290	. . . . . . . . . . . . . . . . . . . 20 |- ((( 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 Sf)))) -> ((( a e. A /\ e e. A) /\ ( b e. B /\ f e. B)) /\ ( a R e \/ ( a = e /\ b Sf))))))
56		breq12 3760	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (( t = <. a , b >. /\ t = <. a , b >.) -> ( t T t <-> <. a , b >. T <. a , b >.))
57	56	anidms 377	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( t = <. a , b >. -> ( t T t <-> <. a , b >. T <. a , b >.))
58	57	notbid 591	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( t = <. a , b >. -> (-. t T t <-> -. <. a , b >. T <. a , b >.))
59	58	3ad2ant1 924	. . . . . . . . . . . . . . . . . . . . . 22 |- (( t = <. a , b >. /\ u = <. c , d >. /\ v = <. e , f >.) -> (-. t T t <-> -. <. a , b >. T <. a , b >.))
60		breq12 3760	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (( t = <. a , b >. /\ u = <. c , d >.) -> ( t Tu <-> <. a , b >. T <. c , d >.))
61	60	3adant3 923	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (( t = <. a , b >. /\ u = <. c , d >. /\ v = <. e , f >.) -> ( t Tu <-> <. a , b >. T <. c , d >.))
62		breq12 3760	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((u = <. c , d >. /\ v = <. e , f >.) -> (u Tv <-> <. c , d >. T <. e , f >.))
63	62	3adant1 921	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (( t = <. a , b >. /\ u = <. c , d >. /\ v = <. e , f >.) -> (u Tv <-> <. c , d >. T <. e , f >.))
64	61, 63	anbi12d 442	. . . . . . . . . . . . . . . . . . . . . . 23 |- (( t = <. a , b >. /\ u = <. c , d >. /\ v = <. e , f >.) -> (( t Tu /\ u Tv) <-> ( <. a , b >. T <. c , d >. /\ <. c , d >. T <. e , f >.)))
65		breq12 3760	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (( t = <. a , b >. /\ v = <. e , f >.) -> ( t Tv <-> <. a , b >. T <. e , f >.))
66	65	3adant2 922	. . . . . . . . . . . . . . . . . . . . . . 23 |- (( t = <. a , b >. /\ u = <. c , d >. /\ v = <. e , f >.) -> ( t Tv <-> <. a , b >. T <. e , f >.))
67	64, 66	imbi12d 223	. . . . . . . . . . . . . . . . . . . . . 22 |- (( t = <. a , b >. /\ u = <. c , d >. /\ v = <. e , f >.) -> ((( t Tu /\ u Tv) -> t Tv) <-> (( <. a , b >. T <. c , d >. /\ <. c , d >. T <. e , f >.) -> <. a , b >. T <. e , f >.)))
68	59, 67	anbi12d 442	. . . . . . . . . . . . . . . . . . . . 21 |- (( t = <. a , b >. /\ u = <. c , d >. /\ v = <. e , f >.) -> ((-. t T t /\ (( t Tu /\ u Tv) -> t Tv)) <-> (-. <. a , b >. T <. a , b >. /\ (( <. a , b >. T <. c , d >. /\ <. c , d >. T <. e , f >.) -> <. a , b >. T <. e , f >.))))
69		poxp.1	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 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)))) }
70	69	xporderlem 5793	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( <. 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 593	. . . . . . . . . . . . . . . . . . . . . 22 |- (-. <. 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	69	xporderlem 5793	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( <. 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	69	xporderlem 5793	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( <. c , d >. T <. e , f >. <-> ((( c e. A /\ e e. A) /\ ( d e. B /\ f e. B)) /\ ( c R e \/ ( c = e /\ d Sf))))
74	72, 73	anbi12i 433	. . . . . . . . . . . . . . . . . . . . . . 23 |- (( <. 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 Sf)))))
75	69	xporderlem 5793	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( <. a , b >. T <. e , f >. <-> ((( a e. A /\ e e. A) /\ ( b e. B /\ f e. B)) /\ ( a R e \/ ( a = e /\ b Sf))))
76	74, 75	imbi12i 228	. . . . . . . . . . . . . . . . . . . . . 22 |- ((( <. 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 Sf)))) -> ((( a e. A /\ e e. A) /\ ( b e. B /\ f e. B)) /\ ( a R e \/ ( a = e /\ b Sf)))))
77	71, 76	anbi12i 433	. . . . . . . . . . . . . . . . . . . . 21 |- ((-. <. 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 Sf)))) -> ((( a e. A /\ e e. A) /\ ( b e. B /\ f e. B)) /\ ( a R e \/ ( a = e /\ b Sf))))))
78	68, 77	syl6bb 185	. . . . . . . . . . . . . . . . . . . 20 |- (( t = <. a , b >. /\ u = <. c , d >. /\ v = <. e , f >.) -> ((-. t T t /\ (( t Tu /\ u Tv) -> t Tv)) <-> (-. ((( 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 Sf)))) -> ((( a e. A /\ e e. A) /\ ( b e. B /\ f e. B)) /\ ( a R e \/ ( a = e /\ b Sf)))))))
79	55, 78	syl5ibr 145	. . . . . . . . . . . . . . . . . . 19 |- (( 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 Tu /\ u Tv) -> t Tv))))
80	79	expcomd 1327	. . . . . . . . . . . . . . . . . 18 |- (( 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 Tu /\ u Tv) -> t Tv)))))
81	80	imp 115	. . . . . . . . . . . . . . . . 17 |- ((( 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 Tu /\ u Tv) -> t Tv))))
82	4, 81	sylbi 114	. . . . . . . . . . . . . . . 16 |- ((( 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 Tu /\ u Tv) -> t Tv))))
83	82	3exp 1102	. . . . . . . . . . . . . . 15 |- (( 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 Tu /\ u Tv) -> t Tv))))))
84	83	com3l 75	. . . . . . . . . . . . . 14 |- ((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 Tu /\ u Tv) -> t Tv))))))
85	84	exlimivv 1773	. . . . . . . . . . . . 13 |- (E. cE. 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 Tu /\ u Tv) -> t Tv))))))
86	85	com3l 75	. . . . . . . . . . . 12 |- ((v = <. e , f >. /\ ( e e. A /\ f e. B)) -> (( t = <. a , b >. /\ ( a e. A /\ b e. B)) -> (E. cE. d(u = <. c , d >. /\ ( c e. A /\ d e. B)) -> (( R Po A /\ S Po B) -> (-. t T t /\ (( t Tu /\ u Tv) -> t Tv))))))
87	86	exlimivv 1773	. . . . . . . . . . 11 |- (E. eE.f(v = <. e , f >. /\ ( e e. A /\ f e. B)) -> (( t = <. a , b >. /\ ( a e. A /\ b e. B)) -> (E. cE. d(u = <. c , d >. /\ ( c e. A /\ d e. B)) -> (( R Po A /\ S Po B) -> (-. t T t /\ (( t Tu /\ u Tv) -> t Tv))))))
88	87	com3l 75	. . . . . . . . . 10 |- (( t = <. a , b >. /\ ( a e. A /\ b e. B)) -> (E. cE. d(u = <. c , d >. /\ ( c e. A /\ d e. B)) -> (E. eE.f(v = <. e , f >. /\ ( e e. A /\ f e. B)) -> (( R Po A /\ S Po B) -> (-. t T t /\ (( t Tu /\ u Tv) -> t Tv))))))
89	88	exlimivv 1773	. . . . . . . . 9 |- (E. aE. b( t = <. a , b >. /\ ( a e. A /\ b e. B)) -> (E. cE. d(u = <. c , d >. /\ ( c e. A /\ d e. B)) -> (E. eE.f(v = <. e , f >. /\ ( e e. A /\ f e. B)) -> (( R Po A /\ S Po B) -> (-. t T t /\ (( t Tu /\ u Tv) -> t Tv))))))
90	89	3imp 1097	. . . . . . . 8 |- ((E. aE. b( t = <. a , b >. /\ ( a e. A /\ b e. B)) /\ E. cE. d(u = <. c , d >. /\ ( c e. A /\ d e. B)) /\ E. eE.f(v = <. e , f >. /\ ( e e. A /\ f e. B))) -> (( R Po A /\ S Po B) -> (-. t T t /\ (( t Tu /\ u Tv) -> t Tv))))
91	1, 2, 3, 90	syl3anb 1177	. . . . . . 7 |- (( 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 Tu /\ u Tv) -> t Tv))))
92	91	3expia 1105	. . . . . 6 |- (( 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 Tu /\ u Tv) -> t Tv)))))
93	92	com3r 73	. . . . 5 |- (( 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 Tu /\ u Tv) -> t Tv)))))
94	93	imp 115	. . . 4 |- ((( 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 Tu /\ u Tv) -> t Tv))))
95	94	ralrimiv 2385	. . 3 |- ((( 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 Tu /\ u Tv) -> t Tv)))
96	95	ralrimivva 2395	. 2 |- (( 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 Tu /\ u Tv) -> t Tv)))
97		df-po 4024	. 2 |- ( 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 Tu /\ u Tv) -> t Tv)))
98	96, 97	sylibr 137	1 |- (( R Po A /\ S Po B) -> T Po (A X. B))

Syntax hints:  -. wn 3   -> wi 4   /\ wa 97   <-> wb 98   \/ wo 628   /\ w3a 884   = wceq 1242  E.wex 1378   e. wcel 1390  A.wral 2300   <.cop 3370   class class class wbr 3755   {copab 3808   Po wpo 4022   X. cxp 4286   ` cfv 4845   1stc1st 5707   2ndc2nd 5708

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935  ax-un 4136

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-sbc 2759  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-mpt 3811  df-id 4021  df-po 4024  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-iota 4810  df-fun 4847  df-fv 4853  df-1st 5709  df-2nd 5710

This theorem is referenced by: (None)