Theorem poxp 13949

Description: A lexicographical ordering of two posets.

Hypotheses

Ref	Expression
poxp.1	|- R Po A
poxp.2	|- S Po B
poxp.3	|- 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	|- T Po (A X. B)

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

Proof of Theorem poxp

Step	Hyp	Ref	Expression
1		3an6 13803	. . . . . . . . . . . . 13 |- (((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))))
2		breq12 3343	. . . . . . . . . . . . . . . . . . . 20 |- ((t = <.a, b>. /\ t = <.a, b>.) -> (tTt <-> <.a, b>.T<.a, b>.))
3	2	anidms 480	. . . . . . . . . . . . . . . . . . 19 |- (t = <.a, b>. -> (tTt <-> <.a, b>.T<.a, b>.))
4	3	notbid 673	. . . . . . . . . . . . . . . . . 18 |- (t = <.a, b>. -> (-. tTt <-> -. <.a, b>.T<.a, b>.))
5	4	3ad2ant1 897	. . . . . . . . . . . . . . . . 17 |- ((t = <.a, b>. /\ u = <.c, d>. /\ v = <.e, f>.) -> (-. tTt <-> -. <.a, b>.T<.a, b>.))
6		breq12 3343	. . . . . . . . . . . . . . . . . . . 20 |- ((t = <.a, b>. /\ u = <.c, d>.) -> (tTu <-> <.a, b>.T<.c, d>.))
7	6	3adant3 896	. . . . . . . . . . . . . . . . . . 19 |- ((t = <.a, b>. /\ u = <.c, d>. /\ v = <.e, f>.) -> (tTu <-> <.a, b>.T<.c, d>.))
8		breq12 3343	. . . . . . . . . . . . . . . . . . . 20 |- ((u = <.c, d>. /\ v = <.e, f>.) -> (uTv <-> <.c, d>.T<.e, f>.))
9	8	3adant1 894	. . . . . . . . . . . . . . . . . . 19 |- ((t = <.a, b>. /\ u = <.c, d>. /\ v = <.e, f>.) -> (uTv <-> <.c, d>.T<.e, f>.))
10	7, 9	anbi12d 690	. . . . . . . . . . . . . . . . . 18 |- ((t = <.a, b>. /\ u = <.c, d>. /\ v = <.e, f>.) -> ((tTu /\ uTv) <-> (<.a, b>.T<.c, d>. /\ <.c, d>.T<.e, f>.)))
11		breq12 3343	. . . . . . . . . . . . . . . . . . 19 |- ((t = <.a, b>. /\ v = <.e, f>.) -> (tTv <-> <.a, b>.T<.e, f>.))
12	11	3adant2 895	. . . . . . . . . . . . . . . . . 18 |- ((t = <.a, b>. /\ u = <.c, d>. /\ v = <.e, f>.) -> (tTv <-> <.a, b>.T<.e, f>.))
13	10, 12	imbi12d 688	. . . . . . . . . . . . . . . . 17 |- ((t = <.a, b>. /\ u = <.c, d>. /\ v = <.e, f>.) -> (((tTu /\ uTv) -> tTv) <-> ((<.a, b>.T<.c, d>. /\ <.c, d>.T<.e, f>.) -> <.a, b>.T<.e, f>.)))
14	5, 13	anbi12d 690	. . . . . . . . . . . . . . . 16 |- ((t = <.a, b>. /\ u = <.c, d>. /\ v = <.e, f>.) -> ((-. tTt /\ ((tTu /\ uTv) -> tTv)) <-> (-. <.a, b>.T<.a, b>. /\ ((<.a, b>.T<.c, d>. /\ <.c, d>.T<.e, f>.) -> <.a, b>.T<.e, f>.))))
15		poxp.3	. . . . . . . . . . . . . . . . . . 19 |- 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))))}
16	15	xporderlem 13948	. . . . . . . . . . . . . . . . . 18 |- (<.a, b>.T<.a, b>. <-> (((a e. A /\ a e. A) /\ (b e. B /\ b e. B)) /\ (aRa \/ (a = a /\ bSb))))
17	16	notbii 204	. . . . . . . . . . . . . . . . 17 |- (-. <.a, b>.T<.a, b>. <-> -. (((a e. A /\ a e. A) /\ (b e. B /\ b e. B)) /\ (aRa \/ (a = a /\ bSb))))
18	15	xporderlem 13948	. . . . . . . . . . . . . . . . . . 19 |- (<.a, b>.T<.c, d>. <-> (((a e. A /\ c e. A) /\ (b e. B /\ d e. B)) /\ (aRc \/ (a = c /\ bSd))))
19	15	xporderlem 13948	. . . . . . . . . . . . . . . . . . 19 |- (<.c, d>.T<.e, f>. <-> (((c e. A /\ e e. A) /\ (d e. B /\ f e. B)) /\ (cRe \/ (c = e /\ dSf))))
20	18, 19	anbi12i 540	. . . . . . . . . . . . . . . . . 18 |- ((<.a, b>.T<.c, d>. /\ <.c, d>.T<.e, f>.) <-> ((((a e. A /\ c e. A) /\ (b e. B /\ d e. B)) /\ (aRc \/ (a = c /\ bSd))) /\ (((c e. A /\ e e. A) /\ (d e. B /\ f e. B)) /\ (cRe \/ (c = e /\ dSf)))))
21	15	xporderlem 13948	. . . . . . . . . . . . . . . . . 18 |- (<.a, b>.T<.e, f>. <-> (((a e. A /\ e e. A) /\ (b e. B /\ f e. B)) /\ (aRe \/ (a = e /\ bSf))))
22	20, 21	imbi12i 205	. . . . . . . . . . . . . . . . 17 |- (((<.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)) /\ (aRc \/ (a = c /\ bSd))) /\ (((c e. A /\ e e. A) /\ (d e. B /\ f e. B)) /\ (cRe \/ (c = e /\ dSf)))) -> (((a e. A /\ e e. A) /\ (b e. B /\ f e. B)) /\ (aRe \/ (a = e /\ bSf)))))
23	17, 22	anbi12i 540	. . . . . . . . . . . . . . . 16 |- ((-. <.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)) /\ (aRa \/ (a = a /\ bSb))) /\ (((((a e. A /\ c e. A) /\ (b e. B /\ d e. B)) /\ (aRc \/ (a = c /\ bSd))) /\ (((c e. A /\ e e. A) /\ (d e. B /\ f e. B)) /\ (cRe \/ (c = e /\ dSf)))) -> (((a e. A /\ e e. A) /\ (b e. B /\ f e. B)) /\ (aRe \/ (a = e /\ bSf))))))
24	14, 23	syl6bb 595	. . . . . . . . . . . . . . 15 |- ((t = <.a, b>. /\ u = <.c, d>. /\ v = <.e, f>.) -> ((-. tTt /\ ((tTu /\ uTv) -> tTv)) <-> (-. (((a e. A /\ a e. A) /\ (b e. B /\ b e. B)) /\ (aRa \/ (a = a /\ bSb))) /\ (((((a e. A /\ c e. A) /\ (b e. B /\ d e. B)) /\ (aRc \/ (a = c /\ bSd))) /\ (((c e. A /\ e e. A) /\ (d e. B /\ f e. B)) /\ (cRe \/ (c = e /\ dSf)))) -> (((a e. A /\ e e. A) /\ (b e. B /\ f e. B)) /\ (aRe \/ (a = e /\ bSf)))))))
25		poxp.1	. . . . . . . . . . . . . . . . . . . . 21 |- R Po A
26		poirr 3597	. . . . . . . . . . . . . . . . . . . . 21 |- ((R Po A /\ a e. A) -> -. aRa)
27	25, 26	mpan 759	. . . . . . . . . . . . . . . . . . . 20 |- (a e. A -> -. aRa)
28		poxp.2	. . . . . . . . . . . . . . . . . . . . . 22 |- S Po B
29		poirr 3597	. . . . . . . . . . . . . . . . . . . . . 22 |- ((S Po B /\ b e. B) -> -. bSb)
30	28, 29	mpan 759	. . . . . . . . . . . . . . . . . . . . 21 |- (b e. B -> -. bSb)
31	30	intnand 757	. . . . . . . . . . . . . . . . . . . 20 |- (b e. B -> -. (a = a /\ bSb))
32	27, 31	anim12i 360	. . . . . . . . . . . . . . . . . . 19 |- ((a e. A /\ b e. B) -> (-. aRa /\ -. (a = a /\ bSb)))
33		ioran 331	. . . . . . . . . . . . . . . . . . 19 |- (-. (aRa \/ (a = a /\ bSb)) <-> (-. aRa /\ -. (a = a /\ bSb)))
34	32, 33	sylibr 217	. . . . . . . . . . . . . . . . . 18 |- ((a e. A /\ b e. B) -> -. (aRa \/ (a = a /\ bSb)))
35	34	intnand 757	. . . . . . . . . . . . . . . . 17 |- ((a e. A /\ b e. B) -> -. (((a e. A /\ a e. A) /\ (b e. B /\ b e. B)) /\ (aRa \/ (a = a /\ bSb))))
36	35	3ad2ant1 897	. . . . . . . . . . . . . . . 16 |- (((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)) /\ (aRa \/ (a = a /\ bSb))))
37		3an6 13803	. . . . . . . . . . . . . . . . . . . 20 |- (((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)))
38		potr 3598	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((R Po A /\ (a e. A /\ c e. A /\ e e. A)) -> ((aRc /\ cRe) -> aRe))
39	25, 38	mpan 759	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((a e. A /\ c e. A /\ e e. A) -> ((aRc /\ cRe) -> aRe))
40	39	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((a e. A /\ c e. A /\ e e. A) /\ (aRc /\ cRe)) -> aRe)
41	40	orcd 294	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((a e. A /\ c e. A /\ e e. A) /\ (aRc /\ cRe)) -> (aRe \/ (a = e /\ bSf)))
42	41	expr 418	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((a e. A /\ c e. A /\ e e. A) /\ aRc) -> (cRe -> (aRe \/ (a = e /\ bSf))))
43		breq2 3342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (c = e -> (aRc <-> aRe))
44	43	biimpa 460	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((c = e /\ aRc) -> aRe)
45	44	orcd 294	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((c = e /\ aRc) -> (aRe \/ (a = e /\ bSf)))
46	45	expcom 403	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (aRc -> (c = e -> (aRe \/ (a = e /\ bSf))))
47	46	adantrd 427	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (aRc -> ((c = e /\ dSf) -> (aRe \/ (a = e /\ bSf))))
48	47	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((a e. A /\ c e. A /\ e e. A) /\ aRc) -> ((c = e /\ dSf) -> (aRe \/ (a = e /\ bSf))))
49	42, 48	jaod 469	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((a e. A /\ c e. A /\ e e. A) /\ aRc) -> ((cRe \/ (c = e /\ dSf)) -> (aRe \/ (a = e /\ bSf))))
50	49	ex 402	. . . . . . . . . . . . . . . . . . . . . 22 |- ((a e. A /\ c e. A /\ e e. A) -> (aRc -> ((cRe \/ (c = e /\ dSf)) -> (aRe \/ (a = e /\ bSf)))))
51		breq1 3341	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (a = c -> (aRe <-> cRe))
52		equequ1 1494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (a = c -> (a = e <-> c = e))
53	52	anbi1d 679	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (a = c -> ((a = e /\ bSf) <-> (c = e /\ bSf)))
54	51, 53	orbi12d 689	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (a = c -> ((aRe \/ (a = e /\ bSf)) <-> (cRe \/ (c = e /\ bSf))))
55	54	imbi2d 674	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (a = c -> (((cRe \/ (c = e /\ dSf)) -> (aRe \/ (a = e /\ bSf))) <-> ((cRe \/ (c = e /\ dSf)) -> (cRe \/ (c = e /\ bSf)))))
56		potr 3598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((S Po B /\ (b e. B /\ d e. B /\ f e. B)) -> ((bSd /\ dSf) -> bSf))
57	28, 56	mpan 759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((b e. B /\ d e. B /\ f e. B) -> ((bSd /\ dSf) -> bSf))
58	57	expdimp 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((b e. B /\ d e. B /\ f e. B) /\ bSd) -> (dSf -> bSf))
59	58	anim2d 620	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((b e. B /\ d e. B /\ f e. B) /\ bSd) -> ((c = e /\ dSf) -> (c = e /\ bSf)))
60	59	orim2d 626	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((b e. B /\ d e. B /\ f e. B) /\ bSd) -> ((cRe \/ (c = e /\ dSf)) -> (cRe \/ (c = e /\ bSf))))
61	55, 60	syl5bir 227	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (a = c -> (((b e. B /\ d e. B /\ f e. B) /\ bSd) -> ((cRe \/ (c = e /\ dSf)) -> (aRe \/ (a = e /\ bSf)))))
62	61	exp3a 405	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (a = c -> ((b e. B /\ d e. B /\ f e. B) -> (bSd -> ((cRe \/ (c = e /\ dSf)) -> (aRe \/ (a = e /\ bSf))))))
63	62	com12 14	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((b e. B /\ d e. B /\ f e. B) -> (a = c -> (bSd -> ((cRe \/ (c = e /\ dSf)) -> (aRe \/ (a = e /\ bSf))))))
64	63	imp3a 388	. . . . . . . . . . . . . . . . . . . . . 22 |- ((b e. B /\ d e. B /\ f e. B) -> ((a = c /\ bSd) -> ((cRe \/ (c = e /\ dSf)) -> (aRe \/ (a = e /\ bSf)))))
65	50, 64	jaao 472	. . . . . . . . . . . . . . . . . . . . 21 |- (((a e. A /\ c e. A /\ e e. A) /\ (b e. B /\ d e. B /\ f e. B)) -> ((aRc \/ (a = c /\ bSd)) -> ((cRe \/ (c = e /\ dSf)) -> (aRe \/ (a = e /\ bSf)))))
66	65	imp3a 388	. . . . . . . . . . . . . . . . . . . 20 |- (((a e. A /\ c e. A /\ e e. A) /\ (b e. B /\ d e. B /\ f e. B)) -> (((aRc \/ (a = c /\ bSd)) /\ (cRe \/ (c = e /\ dSf))) -> (aRe \/ (a = e /\ bSf))))
67	37, 66	sylbi 216	. . . . . . . . . . . . . . . . . . 19 |- (((a e. A /\ b e. B) /\ (c e. A /\ d e. B) /\ (e e. A /\ f e. B)) -> (((aRc \/ (a = c /\ bSd)) /\ (cRe \/ (c = e /\ dSf))) -> (aRe \/ (a = e /\ bSf))))
68		an4 564	. . . . . . . . . . . . . . . . . . . . 21 |- (((a e. A /\ b e. B) /\ (e e. A /\ f e. B)) <-> ((a e. A /\ e e. A) /\ (b e. B /\ f e. B)))
69	68	biimpi 168	. . . . . . . . . . . . . . . . . . . 20 |- (((a e. A /\ b e. B) /\ (e e. A /\ f e. B)) -> ((a e. A /\ e e. A) /\ (b e. B /\ f e. B)))
70	69	3adant2 895	. . . . . . . . . . . . . . . . . . 19 |- (((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)))
71	67, 70	jctild 662	. . . . . . . . . . . . . . . . . 18 |- (((a e. A /\ b e. B) /\ (c e. A /\ d e. B) /\ (e e. A /\ f e. B)) -> (((aRc \/ (a = c /\ bSd)) /\ (cRe \/ (c = e /\ dSf))) -> (((a e. A /\ e e. A) /\ (b e. B /\ f e. B)) /\ (aRe \/ (a = e /\ bSf)))))
72	71	adantld 426	. . . . . . . . . . . . . . . . 17 |- (((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))) /\ ((aRc \/ (a = c /\ bSd)) /\ (cRe \/ (c = e /\ dSf)))) -> (((a e. A /\ e e. A) /\ (b e. B /\ f e. B)) /\ (aRe \/ (a = e /\ bSf)))))
73		an4 564	. . . . . . . . . . . . . . . . 17 |- (((((a e. A /\ c e. A) /\ (b e. B /\ d e. B)) /\ (aRc \/ (a = c /\ bSd))) /\ (((c e. A /\ e e. A) /\ (d e. B /\ f e. B)) /\ (cRe \/ (c = e /\ dSf)))) <-> ((((a e. A /\ c e. A) /\ (b e. B /\ d e. B)) /\ ((c e. A /\ e e. A) /\ (d e. B /\ f e. B))) /\ ((aRc \/ (a = c /\ bSd)) /\ (cRe \/ (c = e /\ dSf)))))
74	72, 73	syl5ib 223	. . . . . . . . . . . . . . . 16 |- (((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)) /\ (aRc \/ (a = c /\ bSd))) /\ (((c e. A /\ e e. A) /\ (d e. B /\ f e. B)) /\ (cRe \/ (c = e /\ dSf)))) -> (((a e. A /\ e e. A) /\ (b e. B /\ f e. B)) /\ (aRe \/ (a = e /\ bSf)))))
75	36, 74	jca 310	. . . . . . . . . . . . . . 15 |- (((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)) /\ (aRa \/ (a = a /\ bSb))) /\ (((((a e. A /\ c e. A) /\ (b e. B /\ d e. B)) /\ (aRc \/ (a = c /\ bSd))) /\ (((c e. A /\ e e. A) /\ (d e. B /\ f e. B)) /\ (cRe \/ (c = e /\ dSf)))) -> (((a e. A /\ e e. A) /\ (b e. B /\ f e. B)) /\ (aRe \/ (a = e /\ bSf))))))
76	24, 75	syl5bir 227	. . . . . . . . . . . . . 14 |- ((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)) -> (-. tTt /\ ((tTu /\ uTv) -> tTv))))
77	76	imp 377	. . . . . . . . . . . . 13 |- (((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))) -> (-. tTt /\ ((tTu /\ uTv) -> tTv)))
78	1, 77	sylbi 216	. . . . . . . . . . . 12 |- (((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))) -> (-. tTt /\ ((tTu /\ uTv) -> tTv)))
79	78	3exp 1066	. . . . . . . . . . 11 |- ((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)) -> (-. tTt /\ ((tTu /\ uTv) -> tTv)))))
80	79	com3l 38	. . . . . . . . . 10 |- ((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)) -> (-. tTt /\ ((tTu /\ uTv) -> tTv)))))
81	80	19.23aivv 1675	. . . . . . . . 9 |- (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)) -> (-. tTt /\ ((tTu /\ uTv) -> tTv)))))
82	81	com3l 38	. . . . . . . 8 |- ((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)) -> (-. tTt /\ ((tTu /\ uTv) -> tTv)))))
83	82	19.23aivv 1675	. . . . . . 7 |- (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)) -> (-. tTt /\ ((tTu /\ uTv) -> tTv)))))
84	83	com3l 38	. . . . . 6 |- ((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)) -> (-. tTt /\ ((tTu /\ uTv) -> tTv)))))
85	84	19.23aivv 1675	. . . . 5 |- (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)) -> (-. tTt /\ ((tTu /\ uTv) -> tTv)))))
86	85	3imp 1061	. . . 4 |- ((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))) -> (-. tTt /\ ((tTu /\ uTv) -> tTv)))
87		elxp 4018	. . . 4 |- (t e. (A X. B) <-> E.aE.b(t = <.a, b>. /\ (a e. A /\ b e. B)))
88		elxp 4018	. . . 4 |- (u e. (A X. B) <-> E.cE.d(u = <.c, d>. /\ (c e. A /\ d e. B)))
89		elxp 4018	. . . 4 |- (v e. (A X. B) <-> E.eE.f(v = <.e, f>. /\ (e e. A /\ f e. B)))
90	86, 87, 88, 89	syl3anb 1140	. . 3 |- ((t e. (A X. B) /\ u e. (A X. B) /\ v e. (A X. B)) -> (-. tTt /\ ((tTu /\ uTv) -> tTv)))
91	90	rgen3 2187	. 2 |- A.t e. (A X. B)A.u e. (A X. B)A.v e. (A X. B)(-. tTt /\ ((tTu /\ uTv) -> tTv))
92		df-po 3591	. 2 |- (T Po (A X. B) <-> A.t e. (A X. B)A.u e. (A X. B)A.v e. (A X. B)(-. tTt /\ ((tTu /\ uTv) -> tTv)))
93	91, 92	mpbir 207	1 |- T Po (A X. B)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326  A.wral 2105  <.cop 3046   class class class wbr 3338  {copab 3395   Po wpo 3589   X. cxp 3984  ` cfv 3998  1stc1st 5018  2ndc2nd 5019

This theorem is referenced by:  soxp 13950

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-po 3591  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fv 4014  df-1st 5020  df-2nd 5021

Copyright terms: Public domain