Metamath Proof Explorer


Theorem fpwwe2lem11

Description: Lemma for fpwwe2 . (Contributed by Mario Carneiro, 18-May-2015) (Proof shortened by Peter Mazsa, 23-Sep-2022) (Revised by AV, 20-Jul-2024)

Ref Expression
Hypotheses fpwwe2.1 W = x r | x A r x × x r We x y x [˙ r -1 y / u]˙ u F r u × u = y
fpwwe2.2 φ A V
fpwwe2.3 φ x A r x × x r We x x F r A
fpwwe2.4 X = dom W
Assertion fpwwe2lem11 φ X dom W

Proof

Step Hyp Ref Expression
1 fpwwe2.1 W = x r | x A r x × x r We x y x [˙ r -1 y / u]˙ u F r u × u = y
2 fpwwe2.2 φ A V
3 fpwwe2.3 φ x A r x × x r We x x F r A
4 fpwwe2.4 X = dom W
5 vex a V
6 5 eldm a dom W s a W s
7 1 2 fpwwe2lem2 φ a W s a A s a × a s We a y a [˙ s -1 y / u]˙ u F s u × u = y
8 7 simprbda φ a W s a A s a × a
9 8 simpld φ a W s a A
10 velpw a 𝒫 A a A
11 9 10 sylibr φ a W s a 𝒫 A
12 11 ex φ a W s a 𝒫 A
13 12 exlimdv φ s a W s a 𝒫 A
14 6 13 syl5bi φ a dom W a 𝒫 A
15 14 ssrdv φ dom W 𝒫 A
16 sspwuni dom W 𝒫 A dom W A
17 15 16 sylib φ dom W A
18 4 17 eqsstrid φ X A
19 vex s V
20 19 elrn s ran W a a W s
21 8 simprd φ a W s s a × a
22 1 relopabiv Rel W
23 22 releldmi a W s a dom W
24 23 adantl φ a W s a dom W
25 elssuni a dom W a dom W
26 24 25 syl φ a W s a dom W
27 26 4 sseqtrrdi φ a W s a X
28 xpss12 a X a X a × a X × X
29 27 27 28 syl2anc φ a W s a × a X × X
30 21 29 sstrd φ a W s s X × X
31 velpw s 𝒫 X × X s X × X
32 30 31 sylibr φ a W s s 𝒫 X × X
33 32 ex φ a W s s 𝒫 X × X
34 33 exlimdv φ a a W s s 𝒫 X × X
35 20 34 syl5bi φ s ran W s 𝒫 X × X
36 35 ssrdv φ ran W 𝒫 X × X
37 sspwuni ran W 𝒫 X × X ran W X × X
38 36 37 sylib φ ran W X × X
39 18 38 jca φ X A ran W X × X
40 n0 n y y n
41 ssel2 n X y n y X
42 41 adantl φ n X y n y X
43 4 eleq2i y X y dom W
44 eluni2 y dom W a dom W y a
45 43 44 bitri y X a dom W y a
46 42 45 sylib φ n X y n a dom W y a
47 5 inex2 n a V
48 47 a1i φ n X y n a W s y a n a V
49 7 simplbda φ a W s s We a y a [˙ s -1 y / u]˙ u F s u × u = y
50 49 simpld φ a W s s We a
51 50 ad2ant2r φ n X y n a W s y a s We a
52 wefr s We a s Fr a
53 51 52 syl φ n X y n a W s y a s Fr a
54 inss2 n a a
55 54 a1i φ n X y n a W s y a n a a
56 simplrr φ n X y n a W s y a y n
57 simprr φ n X y n a W s y a y a
58 inelcm y n y a n a
59 56 57 58 syl2anc φ n X y n a W s y a n a
60 fri n a V s Fr a n a a n a v n a z n a ¬ z s v
61 48 53 55 59 60 syl22anc φ n X y n a W s y a v n a z n a ¬ z s v
62 simprl φ n X y n a W s y a v n a z n a ¬ z s v v n a
63 62 elin1d φ n X y n a W s y a v n a z n a ¬ z s v v n
64 simplrr φ n X y n a W s y a v n a z n a ¬ z s v w n z n a ¬ z s v
65 ralnex z n a ¬ z s v ¬ z n a z s v
66 64 65 sylib φ n X y n a W s y a v n a z n a ¬ z s v w n ¬ z n a z s v
67 df-br w ran W v w v ran W
68 eluni2 w v ran W t ran W w v t
69 67 68 bitri w ran W v t ran W w v t
70 vex t V
71 70 elrn t ran W b b W t
72 df-br w t v w v t
73 simprll φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v w n
74 73 adantr φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v a b s = t b × a w n
75 simprr φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v w t v
76 simp-4l φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v φ
77 simprl φ n X y n a W s y a a W s
78 77 ad2antrr φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v a W s
79 simprlr φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v b W t
80 simprr φ a W s b W t b W t
81 1 2 fpwwe2lem2 φ b W t b A t b × b t We b y b [˙ t -1 y / u]˙ u F t u × u = y
82 81 adantr φ a W s b W t b W t b A t b × b t We b y b [˙ t -1 y / u]˙ u F t u × u = y
83 80 82 mpbid φ a W s b W t b A t b × b t We b y b [˙ t -1 y / u]˙ u F t u × u = y
84 83 simpld φ a W s b W t b A t b × b
85 84 simprd φ a W s b W t t b × b
86 76 78 79 85 syl12anc φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v t b × b
87 86 ssbrd φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v w t v w b × b v
88 75 87 mpd φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v w b × b v
89 brxp w b × b v w b v b
90 89 simplbi w b × b v w b
91 88 90 syl φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v w b
92 91 adantr φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v a b s = t b × a w b
93 62 elin2d φ n X y n a W s y a v n a z n a ¬ z s v v a
94 93 ad2antrr φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v a b s = t b × a v a
95 simplrr φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v a b s = t b × a w t v
96 brinxp2 w t b × a v w b v a w t v
97 92 94 95 96 syl21anbrc φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v a b s = t b × a w t b × a v
98 simprr φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v a b s = t b × a s = t b × a
99 98 breqd φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v a b s = t b × a w s v w t b × a v
100 97 99 mpbird φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v a b s = t b × a w s v
101 76 78 21 syl2anc φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v s a × a
102 101 adantr φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v a b s = t b × a s a × a
103 102 ssbrd φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v a b s = t b × a w s v w a × a v
104 100 103 mpd φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v a b s = t b × a w a × a v
105 brxp w a × a v w a v a
106 105 simplbi w a × a v w a
107 104 106 syl φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v a b s = t b × a w a
108 74 107 elind φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v a b s = t b × a w n a
109 breq1 z = w z s v w s v
110 109 rspcev w n a w s v z n a z s v
111 108 100 110 syl2anc φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v a b s = t b × a z n a z s v
112 73 adantr φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v b a t = s a × b w n
113 simprl φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v b a t = s a × b b a
114 91 adantr φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v b a t = s a × b w b
115 113 114 sseldd φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v b a t = s a × b w a
116 112 115 elind φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v b a t = s a × b w n a
117 simplrr φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v b a t = s a × b w t v
118 simprr φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v b a t = s a × b t = s a × b
119 inss1 s a × b s
120 118 119 eqsstrdi φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v b a t = s a × b t s
121 120 ssbrd φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v b a t = s a × b w t v w s v
122 117 121 mpd φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v b a t = s a × b w s v
123 116 122 110 syl2anc φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v b a t = s a × b z n a z s v
124 2 adantr φ a W s b W t A V
125 3 adantlr φ a W s b W t x A r x × x r We x x F r A
126 simprl φ a W s b W t a W s
127 1 124 125 126 80 fpwwe2lem9 φ a W s b W t a b s = t b × a b a t = s a × b
128 76 78 79 127 syl12anc φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v a b s = t b × a b a t = s a × b
129 111 123 128 mpjaodan φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v z n a z s v
130 129 expr φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w t v z n a z s v
131 72 130 syl5bir φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w v t z n a z s v
132 131 expr φ n X y n a W s y a v n a z n a ¬ z s v w n b W t w v t z n a z s v
133 132 exlimdv φ n X y n a W s y a v n a z n a ¬ z s v w n b b W t w v t z n a z s v
134 71 133 syl5bi φ n X y n a W s y a v n a z n a ¬ z s v w n t ran W w v t z n a z s v
135 134 rexlimdv φ n X y n a W s y a v n a z n a ¬ z s v w n t ran W w v t z n a z s v
136 69 135 syl5bi φ n X y n a W s y a v n a z n a ¬ z s v w n w ran W v z n a z s v
137 66 136 mtod φ n X y n a W s y a v n a z n a ¬ z s v w n ¬ w ran W v
138 137 ralrimiva φ n X y n a W s y a v n a z n a ¬ z s v w n ¬ w ran W v
139 61 63 138 reximssdv φ n X y n a W s y a v n w n ¬ w ran W v
140 139 exp32 φ n X y n a W s y a v n w n ¬ w ran W v
141 140 exlimdv φ n X y n s a W s y a v n w n ¬ w ran W v
142 6 141 syl5bi φ n X y n a dom W y a v n w n ¬ w ran W v
143 142 rexlimdv φ n X y n a dom W y a v n w n ¬ w ran W v
144 46 143 mpd φ n X y n v n w n ¬ w ran W v
145 144 expr φ n X y n v n w n ¬ w ran W v
146 145 exlimdv φ n X y y n v n w n ¬ w ran W v
147 40 146 syl5bi φ n X n v n w n ¬ w ran W v
148 147 expimpd φ n X n v n w n ¬ w ran W v
149 148 alrimiv φ n n X n v n w n ¬ w ran W v
150 df-fr ran W Fr X n n X n v n w n ¬ w ran W v
151 149 150 sylibr φ ran W Fr X
152 4 eleq2i w X w dom W
153 eluni2 w dom W b dom W w b
154 152 153 bitri w X b dom W w b
155 45 154 anbi12i y X w X a dom W y a b dom W w b
156 reeanv a dom W b dom W y a w b a dom W y a b dom W w b
157 155 156 bitr4i y X w X a dom W b dom W y a w b
158 vex b V
159 158 eldm b dom W t b W t
160 6 159 anbi12i a dom W b dom W s a W s t b W t
161 exdistrv s t a W s b W t s a W s t b W t
162 160 161 bitr4i a dom W b dom W s t a W s b W t
163 83 simprd φ a W s b W t t We b y b [˙ t -1 y / u]˙ u F t u × u = y
164 163 simpld φ a W s b W t t We b
165 164 ad2antrr φ a W s b W t y a w b a b s = t b × a t We b
166 weso t We b t Or b
167 165 166 syl φ a W s b W t y a w b a b s = t b × a t Or b
168 simprl φ a W s b W t y a w b a b s = t b × a a b
169 simplrl φ a W s b W t y a w b a b s = t b × a y a
170 168 169 sseldd φ a W s b W t y a w b a b s = t b × a y b
171 simplrr φ a W s b W t y a w b a b s = t b × a w b
172 solin t Or b y b w b y t w y = w w t y
173 167 170 171 172 syl12anc φ a W s b W t y a w b a b s = t b × a y t w y = w w t y
174 22 relelrni b W t t ran W
175 174 ad2antll φ a W s b W t t ran W
176 175 ad2antrr φ a W s b W t y a w b a b s = t b × a t ran W
177 elssuni t ran W t ran W
178 176 177 syl φ a W s b W t y a w b a b s = t b × a t ran W
179 178 ssbrd φ a W s b W t y a w b a b s = t b × a y t w y ran W w
180 idd φ a W s b W t y a w b a b s = t b × a y = w y = w
181 178 ssbrd φ a W s b W t y a w b a b s = t b × a w t y w ran W y
182 179 180 181 3orim123d φ a W s b W t y a w b a b s = t b × a y t w y = w w t y y ran W w y = w w ran W y
183 173 182 mpd φ a W s b W t y a w b a b s = t b × a y ran W w y = w w ran W y
184 50 adantrr φ a W s b W t s We a
185 184 ad2antrr φ a W s b W t y a w b b a t = s a × b s We a
186 weso s We a s Or a
187 185 186 syl φ a W s b W t y a w b b a t = s a × b s Or a
188 simplrl φ a W s b W t y a w b b a t = s a × b y a
189 simprl φ a W s b W t y a w b b a t = s a × b b a
190 simplrr φ a W s b W t y a w b b a t = s a × b w b
191 189 190 sseldd φ a W s b W t y a w b b a t = s a × b w a
192 solin s Or a y a w a y s w y = w w s y
193 187 188 191 192 syl12anc φ a W s b W t y a w b b a t = s a × b y s w y = w w s y
194 22 relelrni a W s s ran W
195 194 ad2antrl φ a W s b W t s ran W
196 195 ad2antrr φ a W s b W t y a w b b a t = s a × b s ran W
197 elssuni s ran W s ran W
198 196 197 syl φ a W s b W t y a w b b a t = s a × b s ran W
199 198 ssbrd φ a W s b W t y a w b b a t = s a × b y s w y ran W w
200 idd φ a W s b W t y a w b b a t = s a × b y = w y = w
201 198 ssbrd φ a W s b W t y a w b b a t = s a × b w s y w ran W y
202 199 200 201 3orim123d φ a W s b W t y a w b b a t = s a × b y s w y = w w s y y ran W w y = w w ran W y
203 193 202 mpd φ a W s b W t y a w b b a t = s a × b y ran W w y = w w ran W y
204 127 adantr φ a W s b W t y a w b a b s = t b × a b a t = s a × b
205 183 203 204 mpjaodan φ a W s b W t y a w b y ran W w y = w w ran W y
206 205 exp31 φ a W s b W t y a w b y ran W w y = w w ran W y
207 206 exlimdvv φ s t a W s b W t y a w b y ran W w y = w w ran W y
208 162 207 syl5bi φ a dom W b dom W y a w b y ran W w y = w w ran W y
209 208 rexlimdvv φ a dom W b dom W y a w b y ran W w y = w w ran W y
210 157 209 syl5bi φ y X w X y ran W w y = w w ran W y
211 210 ralrimivv φ y X w X y ran W w y = w w ran W y
212 dfwe2 ran W We X ran W Fr X y X w X y ran W w y = w w ran W y
213 151 211 212 sylanbrc φ ran W We X
214 1 fpwwe2cbv W = z t | z A t z × z t We z w z [˙ t -1 w / b]˙ b F t b × b = w
215 2 adantr φ a W s A V
216 simpr φ a W s a W s
217 214 215 216 fpwwe2lem3 φ a W s y a s -1 y F s s -1 y × s -1 y = y
218 217 anasss φ a W s y a s -1 y F s s -1 y × s -1 y = y
219 cnvimass ran W -1 y dom ran W
220 2 18 ssexd φ X V
221 220 220 xpexd φ X × X V
222 221 38 ssexd φ ran W V
223 222 adantr φ a W s y a ran W V
224 223 dmexd φ a W s y a dom ran W V
225 ssexg ran W -1 y dom ran W dom ran W V ran W -1 y V
226 219 224 225 sylancr φ a W s y a ran W -1 y V
227 id u = ran W -1 y u = ran W -1 y
228 olc w = y w s y w = y
229 df-br z ran W w z w ran W
230 eluni2 z w ran W t ran W z w t
231 229 230 bitri z ran W w t ran W z w t
232 df-br z t w z w t
233 85 ad2antrr φ a W s b W t w s y w = y y a a b s = t b × a t b × b
234 233 ssbrd φ a W s b W t w s y w = y y a a b s = t b × a z t w z b × b w
235 brxp z b × b w z b w b
236 235 simplbi z b × b w z b
237 234 236 syl6 φ a W s b W t w s y w = y y a a b s = t b × a z t w z b
238 21 adantrr φ a W s b W t s a × a
239 238 ssbrd φ a W s b W t w s y w a × a y
240 239 imp φ a W s b W t w s y w a × a y
241 brxp w a × a y w a y a
242 241 simplbi w a × a y w a
243 240 242 syl φ a W s b W t w s y w a
244 243 a1d φ a W s b W t w s y y a w a
245 elequ1 w = y w a y a
246 245 biimprd w = y y a w a
247 246 adantl φ a W s b W t w = y y a w a
248 244 247 jaodan φ a W s b W t w s y w = y y a w a
249 248 impr φ a W s b W t w s y w = y y a w a
250 249 adantr φ a W s b W t w s y w = y y a a b s = t b × a w a
251 237 250 jctird φ a W s b W t w s y w = y y a a b s = t b × a z t w z b w a
252 brxp z b × a w z b w a
253 251 252 syl6ibr φ a W s b W t w s y w = y y a a b s = t b × a z t w z b × a w
254 253 ancld φ a W s b W t w s y w = y y a a b s = t b × a z t w z t w z b × a w
255 simprr φ a W s b W t w s y w = y y a a b s = t b × a s = t b × a
256 255 breqd φ a W s b W t w s y w = y y a a b s = t b × a z s w z t b × a w
257 brin z t b × a w z t w z b × a w
258 256 257 bitrdi φ a W s b W t w s y w = y y a a b s = t b × a z s w z t w z b × a w
259 254 258 sylibrd φ a W s b W t w s y w = y y a a b s = t b × a z t w z s w
260 simprr φ a W s b W t w s y w = y y a b a t = s a × b t = s a × b
261 260 119 eqsstrdi φ a W s b W t w s y w = y y a b a t = s a × b t s
262 261 ssbrd φ a W s b W t w s y w = y y a b a t = s a × b z t w z s w
263 127 adantr φ a W s b W t w s y w = y y a a b s = t b × a b a t = s a × b
264 259 262 263 mpjaodan φ a W s b W t w s y w = y y a z t w z s w
265 232 264 syl5bir φ a W s b W t w s y w = y y a z w t z s w
266 265 exp32 φ a W s b W t w s y w = y y a z w t z s w
267 266 expr φ a W s b W t w s y w = y y a z w t z s w
268 267 com24 φ a W s y a w s y w = y b W t z w t z s w
269 268 impr φ a W s y a w s y w = y b W t z w t z s w
270 269 imp φ a W s y a w s y w = y b W t z w t z s w
271 270 exlimdv φ a W s y a w s y w = y b b W t z w t z s w
272 71 271 syl5bi φ a W s y a w s y w = y t ran W z w t z s w
273 272 rexlimdv φ a W s y a w s y w = y t ran W z w t z s w
274 231 273 syl5bi φ a W s y a w s y w = y z ran W w z s w
275 228 274 sylan2 φ a W s y a w = y z ran W w z s w
276 275 ex φ a W s y a w = y z ran W w z s w
277 276 alrimiv φ a W s y a w w = y z ran W w z s w
278 breq2 w = y z ran W w z ran W y
279 breq2 w = y z s w z s y
280 278 279 imbi12d w = y z ran W w z s w z ran W y z s y
281 280 equsalvw w w = y z ran W w z s w z ran W y z s y
282 277 281 sylib φ a W s y a z ran W y z s y
283 194 ad2antrl φ a W s y a s ran W
284 283 197 syl φ a W s y a s ran W
285 284 ssbrd φ a W s y a z s y z ran W y
286 282 285 impbid φ a W s y a z ran W y z s y
287 vex z V
288 287 eliniseg y V z ran W -1 y z ran W y
289 288 elv z ran W -1 y z ran W y
290 287 eliniseg y V z s -1 y z s y
291 290 elv z s -1 y z s y
292 286 289 291 3bitr4g φ a W s y a z ran W -1 y z s -1 y
293 292 eqrdv φ a W s y a ran W -1 y = s -1 y
294 227 293 sylan9eqr φ a W s y a u = ran W -1 y u = s -1 y
295 294 sqxpeqd φ a W s y a u = ran W -1 y u × u = s -1 y × s -1 y
296 295 ineq2d φ a W s y a u = ran W -1 y ran W u × u = ran W s -1 y × s -1 y
297 relinxp Rel ran W s -1 y × s -1 y
298 relinxp Rel s s -1 y × s -1 y
299 vex w V
300 299 eliniseg y V w s -1 y w s y
301 290 300 anbi12d y V z s -1 y w s -1 y z s y w s y
302 301 elv z s -1 y w s -1 y z s y w s y
303 orc w s y w s y w = y
304 303 274 sylan2 φ a W s y a w s y z ran W w z s w
305 304 adantrl φ a W s y a z s y w s y z ran W w z s w
306 284 adantr φ a W s y a z s y w s y s ran W
307 306 ssbrd φ a W s y a z s y w s y z s w z ran W w
308 305 307 impbid φ a W s y a z s y w s y z ran W w z s w
309 302 308 sylan2b φ a W s y a z s -1 y w s -1 y z ran W w z s w
310 309 pm5.32da φ a W s y a z s -1 y w s -1 y z ran W w z s -1 y w s -1 y z s w
311 df-br z ran W s -1 y × s -1 y w z w ran W s -1 y × s -1 y
312 brinxp2 z ran W s -1 y × s -1 y w z s -1 y w s -1 y z ran W w
313 311 312 bitr3i z w ran W s -1 y × s -1 y z s -1 y w s -1 y z ran W w
314 df-br z s s -1 y × s -1 y w z w s s -1 y × s -1 y
315 brinxp2 z s s -1 y × s -1 y w z s -1 y w s -1 y z s w
316 314 315 bitr3i z w s s -1 y × s -1 y z s -1 y w s -1 y z s w
317 310 313 316 3bitr4g φ a W s y a z w ran W s -1 y × s -1 y z w s s -1 y × s -1 y
318 297 298 317 eqrelrdv φ a W s y a ran W s -1 y × s -1 y = s s -1 y × s -1 y
319 318 adantr φ a W s y a u = ran W -1 y ran W s -1 y × s -1 y = s s -1 y × s -1 y
320 296 319 eqtrd φ a W s y a u = ran W -1 y ran W u × u = s s -1 y × s -1 y
321 294 320 oveq12d φ a W s y a u = ran W -1 y u F ran W u × u = s -1 y F s s -1 y × s -1 y
322 321 eqeq1d φ a W s y a u = ran W -1 y u F ran W u × u = y s -1 y F s s -1 y × s -1 y = y
323 226 322 sbcied φ a W s y a [˙ ran W -1 y / u]˙ u F ran W u × u = y s -1 y F s s -1 y × s -1 y = y
324 218 323 mpbird φ a W s y a [˙ ran W -1 y / u]˙ u F ran W u × u = y
325 324 exp32 φ a W s y a [˙ ran W -1 y / u]˙ u F ran W u × u = y
326 325 exlimdv φ s a W s y a [˙ ran W -1 y / u]˙ u F ran W u × u = y
327 6 326 syl5bi φ a dom W y a [˙ ran W -1 y / u]˙ u F ran W u × u = y
328 327 rexlimdv φ a dom W y a [˙ ran W -1 y / u]˙ u F ran W u × u = y
329 45 328 syl5bi φ y X [˙ ran W -1 y / u]˙ u F ran W u × u = y
330 329 ralrimiv φ y X [˙ ran W -1 y / u]˙ u F ran W u × u = y
331 213 330 jca φ ran W We X y X [˙ ran W -1 y / u]˙ u F ran W u × u = y
332 1 2 fpwwe2lem2 φ X W ran W X A ran W X × X ran W We X y X [˙ ran W -1 y / u]˙ u F ran W u × u = y
333 39 331 332 mpbir2and φ X W ran W
334 22 releldmi X W ran W X dom W
335 333 334 syl φ X dom W