Metamath Proof Explorer


Theorem fpwwe2lem4

Description: Lemma for fpwwe2 . (Contributed by Mario Carneiro, 15-May-2015) (Revised by AV, 20-Jul-2024) (Proof shortened by Matthew House, 10-Sep-2025)

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
Assertion fpwwe2lem4 φ X A R X × X R We X X F R A

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 2 adantr φ X A R X × X R We X A V
5 simpr1 φ X A R X × X R We X X A
6 4 5 ssexd φ X A R X × X R We X X V
7 6 6 xpexd φ X A R X × X R We X X × X V
8 simpr2 φ X A R X × X R We X R X × X
9 7 8 ssexd φ X A R X × X R We X R V
10 simpl x = X r = R x = X
11 10 sseq1d x = X r = R x A X A
12 simpr x = X r = R r = R
13 10 sqxpeqd x = X r = R x × x = X × X
14 12 13 sseq12d x = X r = R r x × x R X × X
15 12 10 weeq12d x = X r = R r We x R We X
16 11 14 15 3anbi123d x = X r = R x A r x × x r We x X A R X × X R We X
17 oveq12 x = X r = R x F r = X F R
18 17 eleq1d x = X r = R x F r A X F R A
19 16 18 imbi12d x = X r = R x A r x × x r We x x F r A X A R X × X R We X X F R A
20 3 ex φ x A r x × x r We x x F r A
21 20 adantr φ X A R X × X R We X x A r x × x r We x x F r A
22 6 9 19 21 vtocl2d φ X A R X × X R We X X A R X × X R We X X F R A
23 22 syldbl2 φ X A R X × X R We X X F R A