Metamath Proof Explorer


Theorem poxp2

Description: Another way of partially ordering a cross product of two classes. (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Hypotheses xpord2.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 nd x = 2 nd y x y
poxp2.1 φ R Po A
poxp2.2 φ S Po B
Assertion poxp2 φ T Po A × B

Proof

Step Hyp Ref Expression
1 xpord2.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 nd x = 2 nd y x y
2 poxp2.1 φ R Po A
3 poxp2.2 φ S Po B
4 elxp2 a A × B p A q B a = p q
5 equid p = p
6 equid q = q
7 5 6 pm3.2i p = p q = q
8 neorian p p q q ¬ p = p q = q
9 8 con2bii p = p q = q ¬ p p q q
10 7 9 mpbi ¬ p p q q
11 simp3 p R p p = p q S q q = q p p q q p p q q
12 10 11 mto ¬ p R p p = p q S q q = q p p q q
13 simp3 p A q B p A q B p R p p = p q S q q = q p p q q p R p p = p q S q q = q p p q q
14 12 13 mto ¬ p A q B p A q B p R p p = p q S q q = q p p q q
15 1 xpord2lem p q T p q p A q B p A q B p R p p = p q S q q = q p p q q
16 14 15 mtbir ¬ p q T p q
17 breq12 a = p q a = p q a T a p q T p q
18 17 anidms a = p q a T a p q T p q
19 16 18 mtbiri a = p q ¬ a T a
20 19 rexlimivw q B a = p q ¬ a T a
21 20 rexlimivw p A q B a = p q ¬ a T a
22 4 21 sylbi a A × B ¬ a T a
23 22 adantl φ a A × B ¬ a T a
24 3reeanv p A r A t A q B a = p q s B b = r s u B c = t u p A q B a = p q r A s B b = r s t A u B c = t u
25 3reeanv q B s B u B a = p q b = r s c = t u q B a = p q s B b = r s u B c = t u
26 25 rexbii t A q B s B u B a = p q b = r s c = t u t A q B a = p q s B b = r s u B c = t u
27 26 2rexbii p A r A t A q B s B u B a = p q b = r s c = t u p A r A t A q B a = p q s B b = r s u B c = t u
28 elxp2 b A × B r A s B b = r s
29 elxp2 c A × B t A u B c = t u
30 4 28 29 3anbi123i a A × B b A × B c A × B p A q B a = p q r A s B b = r s t A u B c = t u
31 24 27 30 3bitr4ri a A × B b A × B c A × B p A r A t A q B s B u B a = p q b = r s c = t u
32 df-3an p A r A t A q B s B u B p A r A t A q B s B u B
33 simp3 p A q B r A s B p R r p = r q S s q = s p r q s p R r p = r q S s q = s p r q s
34 simp3 r A s B t A u B r R t r = t s S u s = u r t s u r R t r = t s S u s = u r t s u
35 simpr1l φ p A r A t A q B s B u B p A
36 35 adantr φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u p A
37 simpr2r φ p A r A t A q B s B u B q B
38 37 adantr φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u q B
39 36 38 jca φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u p A q B
40 simpr2l φ p A r A t A q B s B u B t A
41 40 adantr φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u t A
42 simpr3r φ p A r A t A q B s B u B u B
43 42 adantr φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u u B
44 41 43 jca φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u t A u B
45 2 ad2antrr φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u R Po A
46 simpr1r φ p A r A t A q B s B u B r A
47 46 adantr φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u r A
48 potr R Po A p A r A t A p R r r R t p R t
49 45 36 47 41 48 syl13anc φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u p R r r R t p R t
50 orc p R t p R t p = t
51 49 50 syl6 φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u p R r r R t p R t p = t
52 51 expd φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u p R r r R t p R t p = t
53 breq1 p = r p R t r R t
54 53 50 syl6bir p = r r R t p R t p = t
55 54 a1i φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u p = r r R t p R t p = t
56 simprl1 φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u p R r p = r
57 52 55 56 mpjaod φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u r R t p R t p = t
58 breq2 r = t p R r p R t
59 equequ2 r = t p = r p = t
60 58 59 orbi12d r = t p R r p = r p R t p = t
61 56 60 syl5ibcom φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u r = t p R t p = t
62 simprr1 φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u r R t r = t
63 57 61 62 mpjaod φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u p R t p = t
64 3 ad2antrr φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u S Po B
65 simpr3l φ p A r A t A q B s B u B s B
66 65 adantr φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u s B
67 potr S Po B q B s B u B q S s s S u q S u
68 64 38 66 43 67 syl13anc φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u q S s s S u q S u
69 orc q S u q S u q = u
70 68 69 syl6 φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u q S s s S u q S u q = u
71 70 expd φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u q S s s S u q S u q = u
72 breq1 q = s q S u s S u
73 72 69 syl6bir q = s s S u q S u q = u
74 73 a1i φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u q = s s S u q S u q = u
75 simprl2 φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u q S s q = s
76 71 74 75 mpjaod φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u s S u q S u q = u
77 breq2 s = u q S s q S u
78 equequ2 s = u q = s q = u
79 77 78 orbi12d s = u q S s q = s q S u q = u
80 75 79 syl5ibcom φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u s = u q S u q = u
81 simprr2 φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u s S u s = u
82 76 80 81 mpjaod φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u q S u q = u
83 simprr3 φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u r t s u
84 neorian r t s u ¬ r = t s = u
85 83 84 sylib φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u ¬ r = t s = u
86 neorian p t q u ¬ p = t q = u
87 86 con2bii p = t q = u ¬ p t q u
88 breq1 p = t p R r t R r
89 equequ1 p = t p = r t = r
90 88 89 orbi12d p = t p R r p = r t R r t = r
91 90 adantr p = t q = u p R r p = r t R r t = r
92 breq1 q = u q S s u S s
93 equequ1 q = u q = s u = s
94 92 93 orbi12d q = u q S s q = s u S s u = s
95 94 adantl p = t q = u q S s q = s u S s u = s
96 neeq1 p = t p r t r
97 96 adantr p = t q = u p r t r
98 neeq1 q = u q s u s
99 98 adantl p = t q = u q s u s
100 97 99 orbi12d p = t q = u p r q s t r u s
101 91 95 100 3anbi123d p = t q = u p R r p = r q S s q = s p r q s t R r t = r u S s u = s t r u s
102 101 anbi1d p = t q = u p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u t R r t = r u S s u = s t r u s r R t r = t s S u s = u r t s u
103 102 anbi2d p = t q = u φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u φ p A r A t A q B s B u B t R r t = r u S s u = s t r u s r R t r = t s S u s = u r t s u
104 simprl1 φ p A r A t A q B s B u B t R r t = r u S s u = s t r u s r R t r = t s S u s = u r t s u t R r t = r
105 simprr1 φ p A r A t A q B s B u B t R r t = r u S s u = s t r u s r R t r = t s S u s = u r t s u r R t r = t
106 orcom t R r r R t r = t r = t t R r r R t
107 ordi r = t t R r r R t r = t t R r r = t r R t
108 orcom r = t t R r t R r r = t
109 equcom r = t t = r
110 109 orbi2i t R r r = t t R r t = r
111 108 110 bitri r = t t R r t R r t = r
112 orcom r = t r R t r R t r = t
113 111 112 anbi12i r = t t R r r = t r R t t R r t = r r R t r = t
114 106 107 113 3bitri t R r r R t r = t t R r t = r r R t r = t
115 104 105 114 sylanbrc φ p A r A t A q B s B u B t R r t = r u S s u = s t r u s r R t r = t s S u s = u r t s u t R r r R t r = t
116 2 ad2antrr φ p A r A t A q B s B u B t R r t = r u S s u = s t r u s r R t r = t s S u s = u r t s u R Po A
117 40 adantr φ p A r A t A q B s B u B t R r t = r u S s u = s t r u s r R t r = t s S u s = u r t s u t A
118 46 adantr φ p A r A t A q B s B u B t R r t = r u S s u = s t r u s r R t r = t s S u s = u r t s u r A
119 po2nr R Po A t A r A ¬ t R r r R t
120 116 117 118 119 syl12anc φ p A r A t A q B s B u B t R r t = r u S s u = s t r u s r R t r = t s S u s = u r t s u ¬ t R r r R t
121 115 120 orcnd φ p A r A t A q B s B u B t R r t = r u S s u = s t r u s r R t r = t s S u s = u r t s u r = t
122 simprl2 φ p A r A t A q B s B u B t R r t = r u S s u = s t r u s r R t r = t s S u s = u r t s u u S s u = s
123 simprr2 φ p A r A t A q B s B u B t R r t = r u S s u = s t r u s r R t r = t s S u s = u r t s u s S u s = u
124 orcom u S s s S u s = u s = u u S s s S u
125 ordi s = u u S s s S u s = u u S s s = u s S u
126 orcom s = u u S s u S s s = u
127 equcom s = u u = s
128 127 orbi2i u S s s = u u S s u = s
129 126 128 bitri s = u u S s u S s u = s
130 orcom s = u s S u s S u s = u
131 129 130 anbi12i s = u u S s s = u s S u u S s u = s s S u s = u
132 124 125 131 3bitri u S s s S u s = u u S s u = s s S u s = u
133 122 123 132 sylanbrc φ p A r A t A q B s B u B t R r t = r u S s u = s t r u s r R t r = t s S u s = u r t s u u S s s S u s = u
134 3 ad2antrr φ p A r A t A q B s B u B t R r t = r u S s u = s t r u s r R t r = t s S u s = u r t s u S Po B
135 42 adantr φ p A r A t A q B s B u B t R r t = r u S s u = s t r u s r R t r = t s S u s = u r t s u u B
136 65 adantr φ p A r A t A q B s B u B t R r t = r u S s u = s t r u s r R t r = t s S u s = u r t s u s B
137 po2nr S Po B u B s B ¬ u S s s S u
138 134 135 136 137 syl12anc φ p A r A t A q B s B u B t R r t = r u S s u = s t r u s r R t r = t s S u s = u r t s u ¬ u S s s S u
139 133 138 orcnd φ p A r A t A q B s B u B t R r t = r u S s u = s t r u s r R t r = t s S u s = u r t s u s = u
140 121 139 jca φ p A r A t A q B s B u B t R r t = r u S s u = s t r u s r R t r = t s S u s = u r t s u r = t s = u
141 103 140 syl6bi p = t q = u φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u r = t s = u
142 141 com12 φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u p = t q = u r = t s = u
143 87 142 syl5bir φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u ¬ p t q u r = t s = u
144 85 143 mt3d φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u p t q u
145 63 82 144 3jca φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u p R t p = t q S u q = u p t q u
146 39 44 145 3jca φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u p A q B t A u B p R t p = t q S u q = u p t q u
147 146 ex φ p A r A t A q B s B u B p R r p = r q S s q = s p r q s r R t r = t s S u s = u r t s u p A q B t A u B p R t p = t q S u q = u p t q u
148 33 34 147 syl2ani φ p A r A t A q B s B u B p A q B r A s B p R r p = r q S s q = s p r q s r A s B t A u B r R t r = t s S u s = u r t s u p A q B t A u B p R t p = t q S u q = u p t q u
149 breq12 a = p q b = r s a T b p q T r s
150 149 3adant3 a = p q b = r s c = t u a T b p q T r s
151 1 xpord2lem p q T r s p A q B r A s B p R r p = r q S s q = s p r q s
152 150 151 bitrdi a = p q b = r s c = t u a T b p A q B r A s B p R r p = r q S s q = s p r q s
153 breq12 b = r s c = t u b T c r s T t u
154 153 3adant1 a = p q b = r s c = t u b T c r s T t u
155 1 xpord2lem r s T t u r A s B t A u B r R t r = t s S u s = u r t s u
156 154 155 bitrdi a = p q b = r s c = t u b T c r A s B t A u B r R t r = t s S u s = u r t s u
157 152 156 anbi12d a = p q b = r s c = t u a T b b T c p A q B r A s B p R r p = r q S s q = s p r q s r A s B t A u B r R t r = t s S u s = u r t s u
158 breq12 a = p q c = t u a T c p q T t u
159 158 3adant2 a = p q b = r s c = t u a T c p q T t u
160 1 xpord2lem p q T t u p A q B t A u B p R t p = t q S u q = u p t q u
161 159 160 bitrdi a = p q b = r s c = t u a T c p A q B t A u B p R t p = t q S u q = u p t q u
162 157 161 imbi12d a = p q b = r s c = t u a T b b T c a T c p A q B r A s B p R r p = r q S s q = s p r q s r A s B t A u B r R t r = t s S u s = u r t s u p A q B t A u B p R t p = t q S u q = u p t q u
163 148 162 syl5ibrcom φ p A r A t A q B s B u B a = p q b = r s c = t u a T b b T c a T c
164 32 163 sylan2br φ p A r A t A q B s B u B a = p q b = r s c = t u a T b b T c a T c
165 164 anassrs φ p A r A t A q B s B u B a = p q b = r s c = t u a T b b T c a T c
166 165 rexlimdvva φ p A r A t A q B s B u B a = p q b = r s c = t u a T b b T c a T c
167 166 anassrs φ p A r A t A q B s B u B a = p q b = r s c = t u a T b b T c a T c
168 167 rexlimdvva φ p A r A t A q B s B u B a = p q b = r s c = t u a T b b T c a T c
169 168 rexlimdvva φ p A r A t A q B s B u B a = p q b = r s c = t u a T b b T c a T c
170 169 imp φ p A r A t A q B s B u B a = p q b = r s c = t u a T b b T c a T c
171 31 170 sylan2b φ a A × B b A × B c A × B a T b b T c a T c
172 23 171 ispod φ T Po A × B