Metamath Proof Explorer


Theorem paireqne

Description: Two sets are not equal iff there is exactly one proper pair whose elements are either one of these sets. (Contributed by AV, 27-Jan-2023)

Ref Expression
Hypotheses paireqne.a φ A V
paireqne.b φ B V
paireqne.p P = x 𝒫 V | x = 2
Assertion paireqne φ ∃! p P x p x = A x = B A B

Proof

Step Hyp Ref Expression
1 paireqne.a φ A V
2 paireqne.b φ B V
3 paireqne.p P = x 𝒫 V | x = 2
4 raleq p = q x p x = A x = B x q x = A x = B
5 4 reu8 ∃! p P x p x = A x = B p P x p x = A x = B q P x q x = A x = B p = q
6 3 eleq2i p P p x 𝒫 V | x = 2
7 elss2prb p x 𝒫 V | x = 2 a V b V a b p = a b
8 6 7 bitri p P a V b V a b p = a b
9 raleq p = a b x p x = A x = B x a b x = A x = B
10 vex a V
11 vex b V
12 eqeq1 x = a x = A a = A
13 eqeq1 x = a x = B a = B
14 12 13 orbi12d x = a x = A x = B a = A a = B
15 eqeq1 x = b x = A b = A
16 eqeq1 x = b x = B b = B
17 15 16 orbi12d x = b x = A x = B b = A b = B
18 10 11 14 17 ralpr x a b x = A x = B a = A a = B b = A b = B
19 9 18 bitrdi p = a b x p x = A x = B a = A a = B b = A b = B
20 eqeq1 p = a b p = q a b = q
21 20 imbi2d p = a b x q x = A x = B p = q x q x = A x = B a b = q
22 21 ralbidv p = a b q P x q x = A x = B p = q q P x q x = A x = B a b = q
23 19 22 anbi12d p = a b x p x = A x = B q P x q x = A x = B p = q a = A a = B b = A b = B q P x q x = A x = B a b = q
24 23 ad2antll φ a V b V a b p = a b x p x = A x = B q P x q x = A x = B p = q a = A a = B b = A b = B q P x q x = A x = B a b = q
25 1 2 jca φ A V B V
26 prelpwi A V B V A B 𝒫 V
27 25 26 syl φ A B 𝒫 V
28 27 ad3antrrr φ a V b V a b p = a b a = A a = B b = A b = B A B 𝒫 V
29 hashprg a V b V a b a b = 2
30 29 adantl φ a V b V a b a b = 2
31 30 biimpd φ a V b V a b a b = 2
32 31 com12 a b φ a V b V a b = 2
33 32 adantr a b p = a b φ a V b V a b = 2
34 33 impcom φ a V b V a b p = a b a b = 2
35 34 adantr φ a V b V a b p = a b a = A a = B b = A b = B a b = 2
36 eqtr3 b = A a = A b = a
37 eqneqall a = b a b p = a b A B = a b
38 37 impd a = b a b p = a b A B = a b
39 38 a1d a = b φ a V b V a b p = a b A B = a b
40 39 impd a = b φ a V b V a b p = a b A B = a b
41 40 equcoms b = a φ a V b V a b p = a b A B = a b
42 36 41 syl b = A a = A φ a V b V a b p = a b A B = a b
43 42 ex b = A a = A φ a V b V a b p = a b A B = a b
44 preq12 a = A b = B a b = A B
45 44 eqcomd a = A b = B A B = a b
46 45 a1d a = A b = B φ a V b V a b p = a b A B = a b
47 46 expcom b = B a = A φ a V b V a b p = a b A B = a b
48 43 47 jaoi b = A b = B a = A φ a V b V a b p = a b A B = a b
49 48 com12 a = A b = A b = B φ a V b V a b p = a b A B = a b
50 prcom a b = b a
51 preq12 b = A a = B b a = A B
52 50 51 syl5eq b = A a = B a b = A B
53 52 eqcomd b = A a = B A B = a b
54 53 a1d b = A a = B φ a V b V a b p = a b A B = a b
55 54 ex b = A a = B φ a V b V a b p = a b A B = a b
56 eqtr3 b = B a = B b = a
57 56 41 syl b = B a = B φ a V b V a b p = a b A B = a b
58 57 ex b = B a = B φ a V b V a b p = a b A B = a b
59 55 58 jaoi b = A b = B a = B φ a V b V a b p = a b A B = a b
60 59 com12 a = B b = A b = B φ a V b V a b p = a b A B = a b
61 49 60 jaoi a = A a = B b = A b = B φ a V b V a b p = a b A B = a b
62 61 imp a = A a = B b = A b = B φ a V b V a b p = a b A B = a b
63 62 impcom φ a V b V a b p = a b a = A a = B b = A b = B A B = a b
64 63 fveqeq2d φ a V b V a b p = a b a = A a = B b = A b = B A B = 2 a b = 2
65 35 64 mpbird φ a V b V a b p = a b a = A a = B b = A b = B A B = 2
66 28 65 jca φ a V b V a b p = a b a = A a = B b = A b = B A B 𝒫 V A B = 2
67 3 eleq2i A B P A B x 𝒫 V | x = 2
68 fveqeq2 x = A B x = 2 A B = 2
69 68 elrab A B x 𝒫 V | x = 2 A B 𝒫 V A B = 2
70 67 69 bitri A B P A B 𝒫 V A B = 2
71 66 70 sylibr φ a V b V a b p = a b a = A a = B b = A b = B A B P
72 raleq q = A B x q x = A x = B x A B x = A x = B
73 eqeq2 q = A B a b = q a b = A B
74 72 73 imbi12d q = A B x q x = A x = B a b = q x A B x = A x = B a b = A B
75 74 rspcv A B P q P x q x = A x = B a b = q x A B x = A x = B a b = A B
76 71 75 syl φ a V b V a b p = a b a = A a = B b = A b = B q P x q x = A x = B a b = q x A B x = A x = B a b = A B
77 eqeq1 x = A x = A A = A
78 eqeq1 x = A x = B A = B
79 77 78 orbi12d x = A x = A x = B A = A A = B
80 eqeq1 x = B x = A B = A
81 eqeq1 x = B x = B B = B
82 80 81 orbi12d x = B x = A x = B B = A B = B
83 79 82 ralprg A V B V x A B x = A x = B A = A A = B B = A B = B
84 25 83 syl φ x A B x = A x = B A = A A = B B = A B = B
85 84 imbi1d φ x A B x = A x = B a b = A B A = A A = B B = A B = B a b = A B
86 85 ad3antrrr φ a V b V a b p = a b a = A a = B b = A b = B x A B x = A x = B a b = A B A = A A = B B = A B = B a b = A B
87 eqid A = A
88 87 orci A = A A = B
89 eqid B = B
90 89 olci B = A B = B
91 pm5.5 A = A A = B B = A B = B A = A A = B B = A B = B a b = A B a b = A B
92 88 90 91 mp2an A = A A = B B = A B = B a b = A B a b = A B
93 10 11 pm3.2i a V b V
94 preq12bg a V b V A V B V a b = A B a = A b = B a = B b = A
95 93 25 94 sylancr φ a b = A B a = A b = B a = B b = A
96 95 adantr φ a V b V a b = A B a = A b = B a = B b = A
97 96 adantr φ a V b V a b p = a b a b = A B a = A b = B a = B b = A
98 eqeq12 a = A b = B a = b A = B
99 98 necon3bid a = A b = B a b A B
100 99 biimpd a = A b = B a b A B
101 eqeq12 a = B b = A a = b B = A
102 101 necon3bid a = B b = A a b B A
103 102 biimpd a = B b = A a b B A
104 necom A B B A
105 103 104 syl6ibr a = B b = A a b A B
106 100 105 jaoi a = A b = B a = B b = A a b A B
107 106 com12 a b a = A b = B a = B b = A A B
108 107 ad2antrl φ a V b V a b p = a b a = A b = B a = B b = A A B
109 97 108 sylbid φ a V b V a b p = a b a b = A B A B
110 109 adantr φ a V b V a b p = a b a = A a = B b = A b = B a b = A B A B
111 92 110 syl5bi φ a V b V a b p = a b a = A a = B b = A b = B A = A A = B B = A B = B a b = A B A B
112 86 111 sylbid φ a V b V a b p = a b a = A a = B b = A b = B x A B x = A x = B a b = A B A B
113 76 112 syld φ a V b V a b p = a b a = A a = B b = A b = B q P x q x = A x = B a b = q A B
114 113 ex φ a V b V a b p = a b a = A a = B b = A b = B q P x q x = A x = B a b = q A B
115 114 impd φ a V b V a b p = a b a = A a = B b = A b = B q P x q x = A x = B a b = q A B
116 24 115 sylbid φ a V b V a b p = a b x p x = A x = B q P x q x = A x = B p = q A B
117 116 ex φ a V b V a b p = a b x p x = A x = B q P x q x = A x = B p = q A B
118 117 rexlimdvva φ a V b V a b p = a b x p x = A x = B q P x q x = A x = B p = q A B
119 8 118 syl5bi φ p P x p x = A x = B q P x q x = A x = B p = q A B
120 119 imp φ p P x p x = A x = B q P x q x = A x = B p = q A B
121 120 rexlimdva φ p P x p x = A x = B q P x q x = A x = B p = q A B
122 5 121 syl5bi φ ∃! p P x p x = A x = B A B
123 27 adantr φ A B A B 𝒫 V
124 hashprg A V B V A B A B = 2
125 25 124 syl φ A B A B = 2
126 125 biimpd φ A B A B = 2
127 126 imp φ A B A B = 2
128 123 127 jca φ A B A B 𝒫 V A B = 2
129 128 70 sylibr φ A B A B P
130 raleq p = A B x p x = A x = B x A B x = A x = B
131 eqeq1 p = A B p = y A B = y
132 131 imbi2d p = A B x y x = A x = B p = y x y x = A x = B A B = y
133 132 ralbidv p = A B y P x y x = A x = B p = y y P x y x = A x = B A B = y
134 130 133 anbi12d p = A B x p x = A x = B y P x y x = A x = B p = y x A B x = A x = B y P x y x = A x = B A B = y
135 134 adantl φ A B p = A B x p x = A x = B y P x y x = A x = B p = y x A B x = A x = B y P x y x = A x = B A B = y
136 vex x V
137 136 elpr x A B x = A x = B
138 137 a1i φ A B x A B x = A x = B
139 138 biimpd φ A B x A B x = A x = B
140 139 imp φ A B x A B x = A x = B
141 140 ralrimiva φ A B x A B x = A x = B
142 3 eleq2i y P y x 𝒫 V | x = 2
143 elss2prb y x 𝒫 V | x = 2 a V b V a b y = a b
144 142 143 bitri y P a V b V a b y = a b
145 prid1g a V a a b
146 145 ad2antrl φ A B a V b V a a b
147 146 adantr φ A B a V b V a b y = a b a a b
148 eleq2 y = a b a y a a b
149 148 ad2antll φ A B a V b V a b y = a b a y a a b
150 147 149 mpbird φ A B a V b V a b y = a b a y
151 14 rspcv a y x y x = A x = B a = A a = B
152 150 151 syl φ A B a V b V a b y = a b x y x = A x = B a = A a = B
153 prid2g b V b a b
154 153 ad2antll φ A B a V b V b a b
155 154 adantr φ A B a V b V a b y = a b b a b
156 eleq2 y = a b b y b a b
157 156 ad2antll φ A B a V b V a b y = a b b y b a b
158 155 157 mpbird φ A B a V b V a b y = a b b y
159 17 rspcv b y x y x = A x = B b = A b = B
160 158 159 syl φ A B a V b V a b y = a b x y x = A x = B b = A b = B
161 simplrr φ A B a V b V a b y = a b b = A b = B a = A a = B y = a b
162 eqtr3 a = A b = A a = b
163 eqneqall a = b a b a b = A B
164 163 com12 a b a = b a b = A B
165 164 ad2antrl φ A B a V b V a b y = a b a = b a b = A B
166 165 com12 a = b φ A B a V b V a b y = a b a b = A B
167 162 166 syl a = A b = A φ A B a V b V a b y = a b a b = A B
168 167 ex a = A b = A φ A B a V b V a b y = a b a b = A B
169 52 a1d b = A a = B φ A B a V b V a b y = a b a b = A B
170 169 expcom a = B b = A φ A B a V b V a b y = a b a b = A B
171 168 170 jaoi a = A a = B b = A φ A B a V b V a b y = a b a b = A B
172 171 com12 b = A a = A a = B φ A B a V b V a b y = a b a b = A B
173 44 a1d a = A b = B φ A B a V b V a b y = a b a b = A B
174 173 ex a = A b = B φ A B a V b V a b y = a b a b = A B
175 eqtr3 a = B b = B a = b
176 175 166 syl a = B b = B φ A B a V b V a b y = a b a b = A B
177 176 ex a = B b = B φ A B a V b V a b y = a b a b = A B
178 174 177 jaoi a = A a = B b = B φ A B a V b V a b y = a b a b = A B
179 178 com12 b = B a = A a = B φ A B a V b V a b y = a b a b = A B
180 172 179 jaoi b = A b = B a = A a = B φ A B a V b V a b y = a b a b = A B
181 180 imp b = A b = B a = A a = B φ A B a V b V a b y = a b a b = A B
182 181 impcom φ A B a V b V a b y = a b b = A b = B a = A a = B a b = A B
183 161 182 eqtr2d φ A B a V b V a b y = a b b = A b = B a = A a = B A B = y
184 183 exp32 φ A B a V b V a b y = a b b = A b = B a = A a = B A B = y
185 160 184 syld φ A B a V b V a b y = a b x y x = A x = B a = A a = B A B = y
186 152 185 mpdd φ A B a V b V a b y = a b x y x = A x = B A B = y
187 186 ex φ A B a V b V a b y = a b x y x = A x = B A B = y
188 187 rexlimdvva φ A B a V b V a b y = a b x y x = A x = B A B = y
189 144 188 syl5bi φ A B y P x y x = A x = B A B = y
190 189 imp φ A B y P x y x = A x = B A B = y
191 190 ralrimiva φ A B y P x y x = A x = B A B = y
192 141 191 jca φ A B x A B x = A x = B y P x y x = A x = B A B = y
193 129 135 192 rspcedvd φ A B p P x p x = A x = B y P x y x = A x = B p = y
194 raleq p = y x p x = A x = B x y x = A x = B
195 194 reu8 ∃! p P x p x = A x = B p P x p x = A x = B y P x y x = A x = B p = y
196 193 195 sylibr φ A B ∃! p P x p x = A x = B
197 196 ex φ A B ∃! p P x p x = A x = B
198 122 197 impbid φ ∃! p P x p x = A x = B A B