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 = x y | x ∈ A × B ∧ y ∈ A × B ∧ 1 st ⁡ x R 1 st ⁡ y ∨ 1 st ⁡ x = 1 st ⁡ y ∧ 2 nd ⁡ x S 2 nd ⁡ y
Assertion soxp ⊢ R Or A ∧ S Or B → T Or A × B

Proof

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