Metamath Proof Explorer


Theorem fpwwelem

Description: Lemma for fpwwe . (Contributed by Mario Carneiro, 15-May-2015) (Revised by AV, 20-Jul-2024)

Ref Expression
Hypotheses fpwwe.1 W = x r | x A r x × x r We x y x F r -1 y = y
fpwwe.2 φ A V
Assertion fpwwelem φ X W R X A R X × X R We X y X F R -1 y = y

Proof

Step Hyp Ref Expression
1 fpwwe.1 W = x r | x A r x × x r We x y x F r -1 y = y
2 fpwwe.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 F R -1 y = y A V
8 simprll φ X A R X × X R We X y X F R -1 y = y X A
9 7 8 ssexd φ X A R X × X R We X y X F R -1 y = y X V
10 9 9 xpexd φ X A R X × X R We X y X F R -1 y = y X × X V
11 simprlr φ X A R X × X R We X y X F R -1 y = y R X × X
12 10 11 ssexd φ X A R X × X R We X y X F R -1 y = y R V
13 9 12 jca φ X A R X × X R We X y X F R -1 y = 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 24 fveqeq2d x = X r = R F r -1 y = y F R -1 y = y
26 14 25 raleqbidv x = X r = R y x F r -1 y = y y X F R -1 y = y
27 22 26 anbi12d x = X r = R r We x y x F r -1 y = y R We X y X F R -1 y = y
28 19 27 anbi12d x = X r = R x A r x × x r We x y x F r -1 y = y X A R X × X R We X y X F R -1 y = y
29 28 1 brabga X V R V X W R X A R X × X R We X y X F R -1 y = y
30 6 13 29 pm5.21nd φ X W R X A R X × X R We X y X F R -1 y = y