Metamath Proof Explorer


Theorem fpwwe2lem10

Description: Lemma for fpwwe2 . (Contributed by Mario Carneiro, 15-May-2015) (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 fpwwe2lem10 φ W : dom W 𝒫 X × X

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 1 relopabiv Rel W
6 5 a1i φ Rel W
7 simprr φ w W s w W t w w s = t w × w s = t w × w
8 1 2 fpwwe2lem2 φ w W t w A t w × w t We w y w [˙ t -1 y / u]˙ u F t u × u = y
9 8 simprbda φ w W t w A t w × w
10 9 simprd φ w W t t w × w
11 10 adantrl φ w W s w W t t w × w
12 11 adantr φ w W s w W t w w s = t w × w t w × w
13 df-ss t w × w t w × w = t
14 12 13 sylib φ w W s w W t w w s = t w × w t w × w = t
15 7 14 eqtrd φ w W s w W t w w s = t w × w s = t
16 simprr φ w W s w W t w w t = s w × w t = s w × w
17 1 2 fpwwe2lem2 φ w W s w A s w × w s We w y w [˙ s -1 y / u]˙ u F s u × u = y
18 17 simprbda φ w W s w A s w × w
19 18 simprd φ w W s s w × w
20 19 adantrr φ w W s w W t s w × w
21 20 adantr φ w W s w W t w w t = s w × w s w × w
22 df-ss s w × w s w × w = s
23 21 22 sylib φ w W s w W t w w t = s w × w s w × w = s
24 16 23 eqtr2d φ w W s w W t w w t = s w × w s = t
25 2 adantr φ w W s w W t A V
26 3 adantlr φ w W s w W t x A r x × x r We x x F r A
27 simprl φ w W s w W t w W s
28 simprr φ w W s w W t w W t
29 1 25 26 27 28 fpwwe2lem9 φ w W s w W t w w s = t w × w w w t = s w × w
30 15 24 29 mpjaodan φ w W s w W t s = t
31 30 ex φ w W s w W t s = t
32 31 alrimiv φ t w W s w W t s = t
33 32 alrimivv φ w s t w W s w W t s = t
34 dffun2 Fun W Rel W w s t w W s w W t s = t
35 6 33 34 sylanbrc φ Fun W
36 35 funfnd φ W Fn dom W
37 vex s V
38 37 elrn s ran W w w W s
39 5 releldmi w W s w dom W
40 39 adantl φ w W s w dom W
41 elssuni w dom W w dom W
42 40 41 syl φ w W s w dom W
43 42 4 sseqtrrdi φ w W s w X
44 xpss12 w X w X w × w X × X
45 43 43 44 syl2anc φ w W s w × w X × X
46 19 45 sstrd φ w W s s X × X
47 46 ex φ w W s s X × X
48 velpw s 𝒫 X × X s X × X
49 47 48 syl6ibr φ w W s s 𝒫 X × X
50 49 exlimdv φ w w W s s 𝒫 X × X
51 38 50 syl5bi φ s ran W s 𝒫 X × X
52 51 ssrdv φ ran W 𝒫 X × X
53 df-f W : dom W 𝒫 X × X W Fn dom W ran W 𝒫 X × X
54 36 52 53 sylanbrc φ W : dom W 𝒫 X × X