Theorem soxp 13950

Description: A lexicographical ordering of two strictly ordered classes.

Hypotheses

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

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

Proof of Theorem soxp

Step	Hyp	Ref	Expression
1		df-so 3604	. 2 |- (T Or (A X. B) <-> (T Po (A X. B) /\ A.t e. (A X. B)A.u e. (A X. B)(tTu \/ t = u \/ uTt)))
2		soxp.1	. . . 4 |- R Or A
3		sopo 3605	. . . 4 |- (R Or A -> R Po A)
4	2, 3	ax-mp 7	. . 3 |- R Po A
5		soxp.2	. . . 4 |- S Or B
6		sopo 3605	. . . 4 |- (S Or B -> S Po B)
7	5, 6	ax-mp 7	. . 3 |- S Po B
8		soxp.3	. . 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))))}
9	4, 7, 8	poxp 13949	. 2 |- T Po (A X. B)
10		breq12 3343	. . . . . . . . . . . . . 14 |- ((t = <.a, b>. /\ u = <.c, d>.) -> (tTu <-> <.a, b>.T<.c, d>.))
11		eqeq12 1896	. . . . . . . . . . . . . 14 |- ((t = <.a, b>. /\ u = <.c, d>.) -> (t = u <-> <.a, b>. = <.c, d>.))
12		breq12 3343	. . . . . . . . . . . . . . 15 |- ((u = <.c, d>. /\ t = <.a, b>.) -> (uTt <-> <.c, d>.T<.a, b>.))
13	12	ancoms 484	. . . . . . . . . . . . . 14 |- ((t = <.a, b>. /\ u = <.c, d>.) -> (uTt <-> <.c, d>.T<.a, b>.))
14	10, 11, 13	3orbi123d 1167	. . . . . . . . . . . . 13 |- ((t = <.a, b>. /\ u = <.c, d>.) -> ((tTu \/ t = u \/ uTt) <-> (<.a, b>.T<.c, d>. \/ <.a, b>. = <.c, d>. \/ <.c, d>.T<.a, b>.)))
15	8	xporderlem 13948	. . . . . . . . . . . . . 14 |- (<.a, b>.T<.c, d>. <-> (((a e. A /\ c e. A) /\ (b e. B /\ d e. B)) /\ (aRc \/ (a = c /\ bSd))))
16		visset 2295	. . . . . . . . . . . . . . 15 |- a e. _V
17		visset 2295	. . . . . . . . . . . . . . 15 |- b e. _V
18		visset 2295	. . . . . . . . . . . . . . 15 |- d e. _V
19	16, 17, 18	opth 3532	. . . . . . . . . . . . . 14 |- (<.a, b>. = <.c, d>. <-> (a = c /\ b = d))
20	8	xporderlem 13948	. . . . . . . . . . . . . 14 |- (<.c, d>.T<.a, b>. <-> (((c e. A /\ a e. A) /\ (d e. B /\ b e. B)) /\ (cRa \/ (c = a /\ dSb))))
21	15, 19, 20	3orbi123i 1057	. . . . . . . . . . . . 13 |- ((<.a, b>.T<.c, d>. \/ <.a, b>. = <.c, d>. \/ <.c, d>.T<.a, b>.) <-> ((((a e. A /\ c e. A) /\ (b e. B /\ d e. B)) /\ (aRc \/ (a = c /\ bSd))) \/ (a = c /\ b = d) \/ (((c e. A /\ a e. A) /\ (d e. B /\ b e. B)) /\ (cRa \/ (c = a /\ dSb)))))
22	14, 21	syl6bb 595	. . . . . . . . . . . 12 |- ((t = <.a, b>. /\ u = <.c, d>.) -> ((tTu \/ t = u \/ uTt) <-> ((((a e. A /\ c e. A) /\ (b e. B /\ d e. B)) /\ (aRc \/ (a = c /\ bSd))) \/ (a = c /\ b = d) \/ (((c e. A /\ a e. A) /\ (d e. B /\ b e. B)) /\ (cRa \/ (c = a /\ dSb))))))
23		solin 3612	. . . . . . . . . . . . . . . . . . . . 21 |- ((R Or A /\ (a e. A /\ c e. A)) -> (aRc \/ a = c \/ cRa))
24	2, 23	mpan 759	. . . . . . . . . . . . . . . . . . . 20 |- ((a e. A /\ c e. A) -> (aRc \/ a = c \/ cRa))
25		3orass 861	. . . . . . . . . . . . . . . . . . . . 21 |- ((aRc \/ a = c \/ cRa) <-> (aRc \/ (a = c \/ cRa)))
26		df-or 241	. . . . . . . . . . . . . . . . . . . . 21 |- ((aRc \/ (a = c \/ cRa)) <-> (-. aRc -> (a = c \/ cRa)))
27	25, 26	bitri 190	. . . . . . . . . . . . . . . . . . . 20 |- ((aRc \/ a = c \/ cRa) <-> (-. aRc -> (a = c \/ cRa)))
28	24, 27	sylib 215	. . . . . . . . . . . . . . . . . . 19 |- ((a e. A /\ c e. A) -> (-. aRc -> (a = c \/ cRa)))
29		solin 3612	. . . . . . . . . . . . . . . . . . . . . 22 |- ((S Or B /\ (b e. B /\ d e. B)) -> (bSd \/ b = d \/ dSb))
30	5, 29	mpan 759	. . . . . . . . . . . . . . . . . . . . 21 |- ((b e. B /\ d e. B) -> (bSd \/ b = d \/ dSb))
31		3orass 861	. . . . . . . . . . . . . . . . . . . . . 22 |- ((bSd \/ b = d \/ dSb) <-> (bSd \/ (b = d \/ dSb)))
32		df-or 241	. . . . . . . . . . . . . . . . . . . . . 22 |- ((bSd \/ (b = d \/ dSb)) <-> (-. bSd -> (b = d \/ dSb)))
33	31, 32	bitri 190	. . . . . . . . . . . . . . . . . . . . 21 |- ((bSd \/ b = d \/ dSb) <-> (-. bSd -> (b = d \/ dSb)))
34	30, 33	sylib 215	. . . . . . . . . . . . . . . . . . . 20 |- ((b e. B /\ d e. B) -> (-. bSd -> (b = d \/ dSb)))
35	34	orim2d 626	. . . . . . . . . . . . . . . . . . 19 |- ((b e. B /\ d e. B) -> ((-. a = c \/ -. bSd) -> (-. a = c \/ (b = d \/ dSb))))
36	28, 35	im2anan9 622	. . . . . . . . . . . . . . . . . 18 |- (((a e. A /\ c e. A) /\ (b e. B /\ d e. B)) -> ((-. aRc /\ (-. a = c \/ -. bSd)) -> ((a = c \/ cRa) /\ (-. a = c \/ (b = d \/ dSb)))))
37		pm2.53 274	. . . . . . . . . . . . . . . . . . . . 21 |- ((a = c \/ cRa) -> (-. a = c -> cRa))
38		orc 291	. . . . . . . . . . . . . . . . . . . . 21 |- (cRa -> (cRa \/ (c = a /\ dSb)))
39	37, 38	syl6 25	. . . . . . . . . . . . . . . . . . . 20 |- ((a = c \/ cRa) -> (-. a = c -> (cRa \/ (c = a /\ dSb))))
40	39	adantr 425	. . . . . . . . . . . . . . . . . . 19 |- (((a = c \/ cRa) /\ (-. a = c \/ (b = d \/ dSb))) -> (-. a = c -> (cRa \/ (c = a /\ dSb))))
41		orel1 271	. . . . . . . . . . . . . . . . . . . . . 22 |- (-. b = d -> ((b = d \/ dSb) -> dSb))
42	41	orim2d 626	. . . . . . . . . . . . . . . . . . . . 21 |- (-. b = d -> ((-. a = c \/ (b = d \/ dSb)) -> (-. a = c \/ dSb)))
43	42	anim2d 620	. . . . . . . . . . . . . . . . . . . 20 |- (-. b = d -> (((a = c \/ cRa) /\ (-. a = c \/ (b = d \/ dSb))) -> ((a = c \/ cRa) /\ (-. a = c \/ dSb))))
44		imor 251	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((a = c -> dSb) <-> (-. a = c \/ dSb))
45	44	biimpri 169	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((-. a = c \/ dSb) -> (a = c -> dSb))
46	45	com12 14	. . . . . . . . . . . . . . . . . . . . . . 23 |- (a = c -> ((-. a = c \/ dSb) -> dSb))
47		equcomi 1487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (a = c -> c = a)
48	47	anim1i 361	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((a = c /\ dSb) -> (c = a /\ dSb))
49	48	olcd 295	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((a = c /\ dSb) -> (cRa \/ (c = a /\ dSb)))
50	49	ex 402	. . . . . . . . . . . . . . . . . . . . . . 23 |- (a = c -> (dSb -> (cRa \/ (c = a /\ dSb))))
51	46, 50	syld 30	. . . . . . . . . . . . . . . . . . . . . 22 |- (a = c -> ((-. a = c \/ dSb) -> (cRa \/ (c = a /\ dSb))))
52	38	a1d 15	. . . . . . . . . . . . . . . . . . . . . 22 |- (cRa -> ((-. a = c \/ dSb) -> (cRa \/ (c = a /\ dSb))))
53	51, 52	jaoi 368	. . . . . . . . . . . . . . . . . . . . 21 |- ((a = c \/ cRa) -> ((-. a = c \/ dSb) -> (cRa \/ (c = a /\ dSb))))
54	53	imp 377	. . . . . . . . . . . . . . . . . . . 20 |- (((a = c \/ cRa) /\ (-. a = c \/ dSb)) -> (cRa \/ (c = a /\ dSb)))
55	43, 54	syl6com 64	. . . . . . . . . . . . . . . . . . 19 |- (((a = c \/ cRa) /\ (-. a = c \/ (b = d \/ dSb))) -> (-. b = d -> (cRa \/ (c = a /\ dSb))))
56	40, 55	jaod 469	. . . . . . . . . . . . . . . . . 18 |- (((a = c \/ cRa) /\ (-. a = c \/ (b = d \/ dSb))) -> ((-. a = c \/ -. b = d) -> (cRa \/ (c = a /\ dSb))))
57	36, 56	syl6 25	. . . . . . . . . . . . . . . . 17 |- (((a e. A /\ c e. A) /\ (b e. B /\ d e. B)) -> ((-. aRc /\ (-. a = c \/ -. bSd)) -> ((-. a = c \/ -. b = d) -> (cRa \/ (c = a /\ dSb)))))
58	57	imp3a 388	. . . . . . . . . . . . . . . 16 |- (((a e. A /\ c e. A) /\ (b e. B /\ d e. B)) -> (((-. aRc /\ (-. a = c \/ -. bSd)) /\ (-. a = c \/ -. b = d)) -> (cRa \/ (c = a /\ dSb))))
59		ioran 331	. . . . . . . . . . . . . . . . 17 |- (-. ((aRc \/ (a = c /\ bSd)) \/ (a = c /\ b = d)) <-> (-. (aRc \/ (a = c /\ bSd)) /\ -. (a = c /\ b = d)))
60		ioran 331	. . . . . . . . . . . . . . . . . . 19 |- (-. (aRc \/ (a = c /\ bSd)) <-> (-. aRc /\ -. (a = c /\ bSd)))
61		ianor 329	. . . . . . . . . . . . . . . . . . . 20 |- (-. (a = c /\ bSd) <-> (-. a = c \/ -. bSd))
62	61	anbi2i 538	. . . . . . . . . . . . . . . . . . 19 |- ((-. aRc /\ -. (a = c /\ bSd)) <-> (-. aRc /\ (-. a = c \/ -. bSd)))
63	60, 62	bitri 190	. . . . . . . . . . . . . . . . . 18 |- (-. (aRc \/ (a = c /\ bSd)) <-> (-. aRc /\ (-. a = c \/ -. bSd)))
64		ianor 329	. . . . . . . . . . . . . . . . . 18 |- (-. (a = c /\ b = d) <-> (-. a = c \/ -. b = d))
65	63, 64	anbi12i 540	. . . . . . . . . . . . . . . . 17 |- ((-. (aRc \/ (a = c /\ bSd)) /\ -. (a = c /\ b = d)) <-> ((-. aRc /\ (-. a = c \/ -. bSd)) /\ (-. a = c \/ -. b = d)))
66	59, 65	bitri 190	. . . . . . . . . . . . . . . 16 |- (-. ((aRc \/ (a = c /\ bSd)) \/ (a = c /\ b = d)) <-> ((-. aRc /\ (-. a = c \/ -. bSd)) /\ (-. a = c \/ -. b = d)))
67	58, 66	syl5ib 223	. . . . . . . . . . . . . . 15 |- (((a e. A /\ c e. A) /\ (b e. B /\ d e. B)) -> (-. ((aRc \/ (a = c /\ bSd)) \/ (a = c /\ b = d)) -> (cRa \/ (c = a /\ dSb))))
68		df-3or 859	. . . . . . . . . . . . . . . 16 |- (((aRc \/ (a = c /\ bSd)) \/ (a = c /\ b = d) \/ (cRa \/ (c = a /\ dSb))) <-> (((aRc \/ (a = c /\ bSd)) \/ (a = c /\ b = d)) \/ (cRa \/ (c = a /\ dSb))))
69		df-or 241	. . . . . . . . . . . . . . . 16 |- ((((aRc \/ (a = c /\ bSd)) \/ (a = c /\ b = d)) \/ (cRa \/ (c = a /\ dSb))) <-> (-. ((aRc \/ (a = c /\ bSd)) \/ (a = c /\ b = d)) -> (cRa \/ (c = a /\ dSb))))
70	68, 69	bitri 190	. . . . . . . . . . . . . . 15 |- (((aRc \/ (a = c /\ bSd)) \/ (a = c /\ b = d) \/ (cRa \/ (c = a /\ dSb))) <-> (-. ((aRc \/ (a = c /\ bSd)) \/ (a = c /\ b = d)) -> (cRa \/ (c = a /\ dSb))))
71	67, 70	sylibr 217	. . . . . . . . . . . . . 14 |- (((a e. A /\ c e. A) /\ (b e. B /\ d e. B)) -> ((aRc \/ (a = c /\ bSd)) \/ (a = c /\ b = d) \/ (cRa \/ (c = a /\ dSb))))
72		pm3.2 305	. . . . . . . . . . . . . . 15 |- (((a e. A /\ c e. A) /\ (b e. B /\ d e. B)) -> ((aRc \/ (a = c /\ bSd)) -> (((a e. A /\ c e. A) /\ (b e. B /\ d e. B)) /\ (aRc \/ (a = c /\ bSd)))))
73		idd 75	. . . . . . . . . . . . . . 15 |- (((a e. A /\ c e. A) /\ (b e. B /\ d e. B)) -> ((a = c /\ b = d) -> (a = c /\ b = d)))
74		pm3.2 305	. . . . . . . . . . . . . . . 16 |- (((c e. A /\ a e. A) /\ (d e. B /\ b e. B)) -> ((cRa \/ (c = a /\ dSb)) -> (((c e. A /\ a e. A) /\ (d e. B /\ b e. B)) /\ (cRa \/ (c = a /\ dSb)))))
75		ancom 482	. . . . . . . . . . . . . . . 16 |- ((a e. A /\ c e. A) <-> (c e. A /\ a e. A))
76		ancom 482	. . . . . . . . . . . . . . . 16 |- ((b e. B /\ d e. B) <-> (d e. B /\ b e. B))
77	74, 75, 76	syl2anb 504	. . . . . . . . . . . . . . 15 |- (((a e. A /\ c e. A) /\ (b e. B /\ d e. B)) -> ((cRa \/ (c = a /\ dSb)) -> (((c e. A /\ a e. A) /\ (d e. B /\ b e. B)) /\ (cRa \/ (c = a /\ dSb)))))
78	72, 73, 77	3orim123d 1176	. . . . . . . . . . . . . 14 |- (((a e. A /\ c e. A) /\ (b e. B /\ d e. B)) -> (((aRc \/ (a = c /\ bSd)) \/ (a = c /\ b = d) \/ (cRa \/ (c = a /\ dSb))) -> ((((a e. A /\ c e. A) /\ (b e. B /\ d e. B)) /\ (aRc \/ (a = c /\ bSd))) \/ (a = c /\ b = d) \/ (((c e. A /\ a e. A) /\ (d e. B /\ b e. B)) /\ (cRa \/ (c = a /\ dSb))))))
79	71, 78	mpd 29	. . . . . . . . . . . . 13 |- (((a e. A /\ c e. A) /\ (b e. B /\ d e. B)) -> ((((a e. A /\ c e. A) /\ (b e. B /\ d e. B)) /\ (aRc \/ (a = c /\ bSd))) \/ (a = c /\ b = d) \/ (((c e. A /\ a e. A) /\ (d e. B /\ b e. B)) /\ (cRa \/ (c = a /\ dSb)))))
80	79	an4s 566	. . . . . . . . . . . 12 |- (((a e. A /\ b e. B) /\ (c e. A /\ d e. B)) -> ((((a e. A /\ c e. A) /\ (b e. B /\ d e. B)) /\ (aRc \/ (a = c /\ bSd))) \/ (a = c /\ b = d) \/ (((c e. A /\ a e. A) /\ (d e. B /\ b e. B)) /\ (cRa \/ (c = a /\ dSb)))))
81	22, 80	syl5bir 227	. . . . . . . . . . 11 |- ((t = <.a, b>. /\ u = <.c, d>.) -> (((a e. A /\ b e. B) /\ (c e. A /\ d e. B)) -> (tTu \/ t = u \/ uTt)))
82	81	imp 377	. . . . . . . . . 10 |- (((t = <.a, b>. /\ u = <.c, d>.) /\ ((a e. A /\ b e. B) /\ (c e. A /\ d e. B))) -> (tTu \/ t = u \/ uTt))
83	82	an4s 566	. . . . . . . . 9 |- (((t = <.a, b>. /\ (a e. A /\ b e. B)) /\ (u = <.c, d>. /\ (c e. A /\ d e. B))) -> (tTu \/ t = u \/ uTt))
84	83	expcom 403	. . . . . . . 8 |- ((u = <.c, d>. /\ (c e. A /\ d e. B)) -> ((t = <.a, b>. /\ (a e. A /\ b e. B)) -> (tTu \/ t = u \/ uTt)))
85	84	19.23aivv 1675	. . . . . . 7 |- (E.cE.d(u = <.c, d>. /\ (c e. A /\ d e. B)) -> ((t = <.a, b>. /\ (a e. A /\ b e. B)) -> (tTu \/ t = u \/ uTt)))
86	85	com12 14	. . . . . 6 |- ((t = <.a, b>. /\ (a e. A /\ b e. B)) -> (E.cE.d(u = <.c, d>. /\ (c e. A /\ d e. B)) -> (tTu \/ t = u \/ uTt)))
87	86	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)) -> (tTu \/ t = u \/ uTt)))
88	87	imp 377	. . . 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))) -> (tTu \/ t = u \/ uTt))
89		elxp 4018	. . . 4 |- (t e. (A X. B) <-> E.aE.b(t = <.a, b>. /\ (a e. A /\ b e. B)))
90		elxp 4018	. . . 4 |- (u e. (A X. B) <-> E.cE.d(u = <.c, d>. /\ (c e. A /\ d e. B)))
91	88, 89, 90	syl2anb 504	. . 3 |- ((t e. (A X. B) /\ u e. (A X. B)) -> (tTu \/ t = u \/ uTt))
92	91	rgen2a 2160	. 2 |- A.t e. (A X. B)A.u e. (A X. B)(tTu \/ t = u \/ uTt)
93	1, 9, 92	mpbir2an 800	1 |- T Or (A X. B)

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

This theorem is referenced by:  wexp 13952

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-3or 859  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-so 3604  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