Metamath Proof Explorer


Theorem fpwwecbv

Description: Lemma for fpwwe . (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Hypothesis fpwwe.1 W = x r | x A r x × x r We x y x F r -1 y = y
Assertion fpwwecbv W = a s | a A s a × a s We a z a F s -1 z = z

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 simpl x = a r = s x = a
3 2 sseq1d x = a r = s x A a A
4 simpr x = a r = s r = s
5 2 sqxpeqd x = a r = s x × x = a × a
6 4 5 sseq12d x = a r = s r x × x s a × a
7 3 6 anbi12d x = a r = s x A r x × x a A s a × a
8 4 2 weeq12d x = a r = s r We x s We a
9 sneq y = z y = z
10 9 imaeq2d y = z r -1 y = r -1 z
11 10 fveq2d y = z F r -1 y = F r -1 z
12 id y = z y = z
13 11 12 eqeq12d y = z F r -1 y = y F r -1 z = z
14 13 cbvralvw y x F r -1 y = y z x F r -1 z = z
15 4 cnveqd x = a r = s r -1 = s -1
16 15 imaeq1d x = a r = s r -1 z = s -1 z
17 16 fveqeq2d x = a r = s F r -1 z = z F s -1 z = z
18 2 17 raleqbidv x = a r = s z x F r -1 z = z z a F s -1 z = z
19 14 18 bitrid x = a r = s y x F r -1 y = y z a F s -1 z = z
20 8 19 anbi12d x = a r = s r We x y x F r -1 y = y s We a z a F s -1 z = z
21 7 20 anbi12d x = a r = s x A r x × x r We x y x F r -1 y = y a A s a × a s We a z a F s -1 z = z
22 21 cbvopabv x r | x A r x × x r We x y x F r -1 y = y = a s | a A s a × a s We a z a F s -1 z = z
23 1 22 eqtri W = a s | a A s a × a s We a z a F s -1 z = z