Metamath Proof Explorer

Theorem soxp

Description: A lexicographical ordering of two strictly ordered classes. (Contributed by Scott Fenton, 17-Mar-2011) (Revised by Mario Carneiro, 7-Mar-2013)

Ref Expression
Hypothesis soxp.1 ⊢T=xy|x∈A×B∧y∈A×B∧1st⁡xR1st⁡y∨1st⁡x=1st⁡y∧2nd⁡xS2nd⁡y
Assertion soxp ⊢ROrA∧SOrB→TOrA×B

Proof

Step Hyp Ref Expression
1 soxp.1 ⊢T=xy|x∈A×B∧y∈A×B∧1st⁡xR1st⁡y∨1st⁡x=1st⁡y∧2nd⁡xS2nd⁡y
2 sopo ⊢ROrA→RPoA
3 sopo ⊢SOrB→SPoB
4 1 poxp ⊢RPoA∧SPoB→TPoA×B
5 2 3 4 syl2an ⊢ROrA∧SOrB→TPoA×B
6 elxp ⊢t∈A×B↔∃a∃bt=ab∧a∈A∧b∈B
7 elxp ⊢u∈A×B↔∃c∃du=cd∧c∈A∧d∈B
8 ioran ⊢¬aRc∨a=c∧bSd∨a=c∧b=d↔¬aRc∨a=c∧bSd∧¬a=c∧b=d
9 ioran ⊢¬aRc∨a=c∧bSd↔¬aRc∧¬a=c∧bSd
10 ianor ⊢¬a=c∧bSd↔¬a=c∨¬bSd
11 10 anbi2i ⊢¬aRc∧¬a=c∧bSd↔¬aRc∧¬a=c∨¬bSd
12 9 11 bitri ⊢¬aRc∨a=c∧bSd↔¬aRc∧¬a=c∨¬bSd
13 ianor ⊢¬a=c∧b=d↔¬a=c∨¬b=d
14 12 13 anbi12i ⊢¬aRc∨a=c∧bSd∧¬a=c∧b=d↔¬aRc∧¬a=c∨¬bSd∧¬a=c∨¬b=d
15 8 14 bitri ⊢¬aRc∨a=c∧bSd∨a=c∧b=d↔¬aRc∧¬a=c∨¬bSd∧¬a=c∨¬b=d
16 solin ⊢ROrA∧a∈A∧c∈A→aRc∨a=c∨cRa
17 3orass ⊢aRc∨a=c∨cRa↔aRc∨a=c∨cRa
18 df-or ⊢aRc∨a=c∨cRa↔¬aRc→a=c∨cRa
19 17 18 bitri ⊢aRc∨a=c∨cRa↔¬aRc→a=c∨cRa
20 16 19 sylib ⊢ROrA∧a∈A∧c∈A→¬aRc→a=c∨cRa
21 solin ⊢SOrB∧b∈B∧d∈B→bSd∨b=d∨dSb
22 3orass ⊢bSd∨b=d∨dSb↔bSd∨b=d∨dSb
23 df-or ⊢bSd∨b=d∨dSb↔¬bSd→b=d∨dSb
24 22 23 bitri ⊢bSd∨b=d∨dSb↔¬bSd→b=d∨dSb
25 21 24 sylib ⊢SOrB∧b∈B∧d∈B→¬bSd→b=d∨dSb
26 25 orim2d ⊢SOrB∧b∈B∧d∈B→¬a=c∨¬bSd→¬a=c∨b=d∨dSb
27 20 26 im2anan9 ⊢ROrA∧a∈A∧c∈A∧SOrB∧b∈B∧d∈B→¬aRc∧¬a=c∨¬bSd→a=c∨cRa∧¬a=c∨b=d∨dSb
28 pm2.53 ⊢a=c∨cRa→¬a=c→cRa
29 orc ⊢cRa→cRa∨c=a∧dSb
30 28 29 syl6 ⊢a=c∨cRa→¬a=c→cRa∨c=a∧dSb
31 30 adantr ⊢a=c∨cRa∧¬a=c∨b=d∨dSb→¬a=c→cRa∨c=a∧dSb
32 orel1 ⊢¬b=d→b=d∨dSb→dSb
33 32 orim2d ⊢¬b=d→¬a=c∨b=d∨dSb→¬a=c∨dSb
34 33 anim2d ⊢¬b=d→a=c∨cRa∧¬a=c∨b=d∨dSb→a=c∨cRa∧¬a=c∨dSb
35 imor ⊢a=c→dSb↔¬a=c∨dSb
36 35 biimpri ⊢¬a=c∨dSb→a=c→dSb
37 36 com12 ⊢a=c→¬a=c∨dSb→dSb
38 equcomi ⊢a=c→c=a
39 38 anim1i ⊢a=c∧dSb→c=a∧dSb
40 39 olcd ⊢a=c∧dSb→cRa∨c=a∧dSb
41 40 ex ⊢a=c→dSb→cRa∨c=a∧dSb
42 37 41 syld ⊢a=c→¬a=c∨dSb→cRa∨c=a∧dSb
43 29 a1d ⊢cRa→¬a=c∨dSb→cRa∨c=a∧dSb
44 42 43 jaoi ⊢a=c∨cRa→¬a=c∨dSb→cRa∨c=a∧dSb
45 44 imp ⊢a=c∨cRa∧¬a=c∨dSb→cRa∨c=a∧dSb
46 34 45 syl6com ⊢a=c∨cRa∧¬a=c∨b=d∨dSb→¬b=d→cRa∨c=a∧dSb
47 31 46 jaod ⊢a=c∨cRa∧¬a=c∨b=d∨dSb→¬a=c∨¬b=d→cRa∨c=a∧dSb
48 27 47 syl6 ⊢ROrA∧a∈A∧c∈A∧SOrB∧b∈B∧d∈B→¬aRc∧¬a=c∨¬bSd→¬a=c∨¬b=d→cRa∨c=a∧dSb
49 48 impd ⊢ROrA∧a∈A∧c∈A∧SOrB∧b∈B∧d∈B→¬aRc∧¬a=c∨¬bSd∧¬a=c∨¬b=d→cRa∨c=a∧dSb
50 15 49 biimtrid ⊢ROrA∧a∈A∧c∈A∧SOrB∧b∈B∧d∈B→¬aRc∨a=c∧bSd∨a=c∧b=d→cRa∨c=a∧dSb
51 df-3or ⊢aRc∨a=c∧bSd∨a=c∧b=d∨cRa∨c=a∧dSb↔aRc∨a=c∧bSd∨a=c∧b=d∨cRa∨c=a∧dSb
52 df-or ⊢aRc∨a=c∧bSd∨a=c∧b=d∨cRa∨c=a∧dSb↔¬aRc∨a=c∧bSd∨a=c∧b=d→cRa∨c=a∧dSb
53 51 52 bitri ⊢aRc∨a=c∧bSd∨a=c∧b=d∨cRa∨c=a∧dSb↔¬aRc∨a=c∧bSd∨a=c∧b=d→cRa∨c=a∧dSb
54 50 53 sylibr ⊢ROrA∧a∈A∧c∈A∧SOrB∧b∈B∧d∈B→aRc∨a=c∧bSd∨a=c∧b=d∨cRa∨c=a∧dSb
55 pm3.2 ⊢a∈A∧c∈A∧b∈B∧d∈B→aRc∨a=c∧bSd→a∈A∧c∈A∧b∈B∧d∈B∧aRc∨a=c∧bSd
56 55 ad2ant2l ⊢ROrA∧a∈A∧c∈A∧SOrB∧b∈B∧d∈B→aRc∨a=c∧bSd→a∈A∧c∈A∧b∈B∧d∈B∧aRc∨a=c∧bSd
57 idd ⊢ROrA∧a∈A∧c∈A∧SOrB∧b∈B∧d∈B→a=c∧b=d→a=c∧b=d
58 simpr ⊢ROrA∧a∈A∧c∈A→a∈A∧c∈A
59 58 ancomd ⊢ROrA∧a∈A∧c∈A→c∈A∧a∈A
60 simpr ⊢SOrB∧b∈B∧d∈B→b∈B∧d∈B
61 60 ancomd ⊢SOrB∧b∈B∧d∈B→d∈B∧b∈B
62 pm3.2 ⊢c∈A∧a∈A∧d∈B∧b∈B→cRa∨c=a∧dSb→c∈A∧a∈A∧d∈B∧b∈B∧cRa∨c=a∧dSb
63 59 61 62 syl2an ⊢ROrA∧a∈A∧c∈A∧SOrB∧b∈B∧d∈B→cRa∨c=a∧dSb→c∈A∧a∈A∧d∈B∧b∈B∧cRa∨c=a∧dSb
64 56 57 63 3orim123d ⊢ROrA∧a∈A∧c∈A∧SOrB∧b∈B∧d∈B→aRc∨a=c∧bSd∨a=c∧b=d∨cRa∨c=a∧dSb→a∈A∧c∈A∧b∈B∧d∈B∧aRc∨a=c∧bSd∨a=c∧b=d∨c∈A∧a∈A∧d∈B∧b∈B∧cRa∨c=a∧dSb
65 54 64 mpd ⊢ROrA∧a∈A∧c∈A∧SOrB∧b∈B∧d∈B→a∈A∧c∈A∧b∈B∧d∈B∧aRc∨a=c∧bSd∨a=c∧b=d∨c∈A∧a∈A∧d∈B∧b∈B∧cRa∨c=a∧dSb
66 65 an4s ⊢ROrA∧SOrB∧a∈A∧c∈A∧b∈B∧d∈B→a∈A∧c∈A∧b∈B∧d∈B∧aRc∨a=c∧bSd∨a=c∧b=d∨c∈A∧a∈A∧d∈B∧b∈B∧cRa∨c=a∧dSb
67 66 expcom ⊢a∈A∧c∈A∧b∈B∧d∈B→ROrA∧SOrB→a∈A∧c∈A∧b∈B∧d∈B∧aRc∨a=c∧bSd∨a=c∧b=d∨c∈A∧a∈A∧d∈B∧b∈B∧cRa∨c=a∧dSb
68 67 an4s ⊢a∈A∧b∈B∧c∈A∧d∈B→ROrA∧SOrB→a∈A∧c∈A∧b∈B∧d∈B∧aRc∨a=c∧bSd∨a=c∧b=d∨c∈A∧a∈A∧d∈B∧b∈B∧cRa∨c=a∧dSb
69 breq12 ⊢t=ab∧u=cd→tTu↔abTcd
70 eqeq12 ⊢t=ab∧u=cd→t=u↔ab=cd
71 breq12 ⊢u=cd∧t=ab→uTt↔cdTab
72 71 ancoms ⊢t=ab∧u=cd→uTt↔cdTab
73 69 70 72 3orbi123d ⊢t=ab∧u=cd→tTu∨t=u∨uTt↔abTcd∨ab=cd∨cdTab
74 1 xporderlem ⊢abTcd↔a∈A∧c∈A∧b∈B∧d∈B∧aRc∨a=c∧bSd
75 vex ⊢a∈V
76 vex ⊢b∈V
77 75 76 opth ⊢ab=cd↔a=c∧b=d
78 1 xporderlem ⊢cdTab↔c∈A∧a∈A∧d∈B∧b∈B∧cRa∨c=a∧dSb
79 74 77 78 3orbi123i ⊢abTcd∨ab=cd∨cdTab↔a∈A∧c∈A∧b∈B∧d∈B∧aRc∨a=c∧bSd∨a=c∧b=d∨c∈A∧a∈A∧d∈B∧b∈B∧cRa∨c=a∧dSb
80 73 79 bitrdi ⊢t=ab∧u=cd→tTu∨t=u∨uTt↔a∈A∧c∈A∧b∈B∧d∈B∧aRc∨a=c∧bSd∨a=c∧b=d∨c∈A∧a∈A∧d∈B∧b∈B∧cRa∨c=a∧dSb
81 80 biimprcd ⊢a∈A∧c∈A∧b∈B∧d∈B∧aRc∨a=c∧bSd∨a=c∧b=d∨c∈A∧a∈A∧d∈B∧b∈B∧cRa∨c=a∧dSb→t=ab∧u=cd→tTu∨t=u∨uTt
82 68 81 syl6 ⊢a∈A∧b∈B∧c∈A∧d∈B→ROrA∧SOrB→t=ab∧u=cd→tTu∨t=u∨uTt
83 82 com3r ⊢t=ab∧u=cd→a∈A∧b∈B∧c∈A∧d∈B→ROrA∧SOrB→tTu∨t=u∨uTt
84 83 imp ⊢t=ab∧u=cd∧a∈A∧b∈B∧c∈A∧d∈B→ROrA∧SOrB→tTu∨t=u∨uTt
85 84 an4s ⊢t=ab∧a∈A∧b∈B∧u=cd∧c∈A∧d∈B→ROrA∧SOrB→tTu∨t=u∨uTt
86 85 expcom ⊢u=cd∧c∈A∧d∈B→t=ab∧a∈A∧b∈B→ROrA∧SOrB→tTu∨t=u∨uTt
87 86 exlimivv ⊢∃c∃du=cd∧c∈A∧d∈B→t=ab∧a∈A∧b∈B→ROrA∧SOrB→tTu∨t=u∨uTt
88 87 com12 ⊢t=ab∧a∈A∧b∈B→∃c∃du=cd∧c∈A∧d∈B→ROrA∧SOrB→tTu∨t=u∨uTt
89 88 exlimivv ⊢∃a∃bt=ab∧a∈A∧b∈B→∃c∃du=cd∧c∈A∧d∈B→ROrA∧SOrB→tTu∨t=u∨uTt
90 89 imp ⊢∃a∃bt=ab∧a∈A∧b∈B∧∃c∃du=cd∧c∈A∧d∈B→ROrA∧SOrB→tTu∨t=u∨uTt
91 6 7 90 syl2anb ⊢t∈A×B∧u∈A×B→ROrA∧SOrB→tTu∨t=u∨uTt
92 91 com12 ⊢ROrA∧SOrB→t∈A×B∧u∈A×B→tTu∨t=u∨uTt
93 92 ralrimivv ⊢ROrA∧SOrB→∀t∈A×B∀u∈A×BtTu∨t=u∨uTt
94 df-so ⊢TOrA×B↔TPoA×B∧∀t∈A×B∀u∈A×BtTu∨t=u∨uTt
95 5 93 94 sylanbrc ⊢ROrA∧SOrB→TOrA×B