Metamath Proof Explorer


Theorem fpwwe2lem2

Description: Lemma for fpwwe2 . (Contributed by Mario Carneiro, 19-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
Assertion fpwwe2lem2 φ X W R X A R X × X R We X y X [˙ R -1 y / u]˙ u F R u × u = y

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 1 relopabiv Rel W
4 3 a1i φ Rel W
5 brrelex12 Rel W X W R X V R V
6 4 5 sylan φ X W R X V R V
7 2 adantr φ X A R X × X R We X y X [˙ R -1 y / u]˙ u F R u × u = y A V
8 simprll φ X A R X × X R We X y X [˙ R -1 y / u]˙ u F R u × u = y X A
9 7 8 ssexd φ X A R X × X R We X y X [˙ R -1 y / u]˙ u F R u × u = y X V
10 9 9 xpexd φ X A R X × X R We X y X [˙ R -1 y / u]˙ u F R u × u = y X × X V
11 simprlr φ X A R X × X R We X y X [˙ R -1 y / u]˙ u F R u × u = y R X × X
12 10 11 ssexd φ X A R X × X R We X y X [˙ R -1 y / u]˙ u F R u × u = y R V
13 9 12 jca φ X A R X × X R We X y X [˙ R -1 y / u]˙ u F R u × u = y X V R V
14 simpl x = X r = R x = X
15 14 sseq1d x = X r = R x A X A
16 simpr x = X r = R r = R
17 14 sqxpeqd x = X r = R x × x = X × X
18 16 17 sseq12d x = X r = R r x × x R X × X
19 15 18 anbi12d x = X r = R x A r x × x X A R X × X
20 weeq2 x = X r We x r We X
21 weeq1 r = R r We X R We X
22 20 21 sylan9bb x = X r = R r We x R We X
23 16 cnveqd x = X r = R r -1 = R -1
24 23 imaeq1d x = X r = R r -1 y = R -1 y
25 16 ineq1d x = X r = R r u × u = R u × u
26 25 oveq2d x = X r = R u F r u × u = u F R u × u
27 26 eqeq1d x = X r = R u F r u × u = y u F R u × u = y
28 24 27 sbceqbid x = X r = R [˙ r -1 y / u]˙ u F r u × u = y [˙ R -1 y / u]˙ u F R u × u = y
29 14 28 raleqbidv x = X r = R y x [˙ r -1 y / u]˙ u F r u × u = y y X [˙ R -1 y / u]˙ u F R u × u = y
30 22 29 anbi12d x = X r = R r We x y x [˙ r -1 y / u]˙ u F r u × u = y R We X y X [˙ R -1 y / u]˙ u F R u × u = y
31 19 30 anbi12d x = X r = R x A r x × x r We x y x [˙ r -1 y / u]˙ u F r u × u = y X A R X × X R We X y X [˙ R -1 y / u]˙ u F R u × u = y
32 31 1 brabga X V R V X W R X A R X × X R We X y X [˙ R -1 y / u]˙ u F R u × u = y
33 6 13 32 pm5.21nd φ X W R X A R X × X R We X y X [˙ R -1 y / u]˙ u F R u × u = y