Metamath Proof Explorer


Theorem aceq3lem

Description: Lemma for dfac3 . (Contributed by NM, 2-Apr-2004) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Hypothesis aceq3lem.1 F = w dom y f u | w y u
Assertion aceq3lem x f z x z f z z f f y f Fn dom y

Proof

Step Hyp Ref Expression
1 aceq3lem.1 F = w dom y f u | w y u
2 vex y V
3 2 rnex ran y V
4 3 pwex 𝒫 ran y V
5 raleq x = 𝒫 ran y z x z f z z z 𝒫 ran y z f z z
6 5 exbidv x = 𝒫 ran y f z x z f z z f z 𝒫 ran y z f z z
7 4 6 spcv x f z x z f z z f z 𝒫 ran y z f z z
8 df-mpt w dom y f u | w y u = w h | w dom y h = f u | w y u
9 1 8 eqtri F = w h | w dom y h = f u | w y u
10 vex w V
11 10 eldm w dom y u w y u
12 abn0 u | w y u u w y u
13 11 12 bitr4i w dom y u | w y u
14 vex u V
15 10 14 brelrn w y u u ran y
16 15 abssi u | w y u ran y
17 3 16 elpwi2 u | w y u 𝒫 ran y
18 neeq1 z = u | w y u z u | w y u
19 fveq2 z = u | w y u f z = f u | w y u
20 id z = u | w y u z = u | w y u
21 19 20 eleq12d z = u | w y u f z z f u | w y u u | w y u
22 18 21 imbi12d z = u | w y u z f z z u | w y u f u | w y u u | w y u
23 22 rspcv u | w y u 𝒫 ran y z 𝒫 ran y z f z z u | w y u f u | w y u u | w y u
24 17 23 ax-mp z 𝒫 ran y z f z z u | w y u f u | w y u u | w y u
25 13 24 syl5bi z 𝒫 ran y z f z z w dom y f u | w y u u | w y u
26 25 imp z 𝒫 ran y z f z z w dom y f u | w y u u | w y u
27 fvex f u | w y u V
28 breq2 z = f u | w y u w y z w y f u | w y u
29 breq2 u = z w y u w y z
30 29 cbvabv u | w y u = z | w y z
31 27 28 30 elab2 f u | w y u u | w y u w y f u | w y u
32 26 31 sylib z 𝒫 ran y z f z z w dom y w y f u | w y u
33 breq2 h = f u | w y u w y h w y f u | w y u
34 32 33 syl5ibrcom z 𝒫 ran y z f z z w dom y h = f u | w y u w y h
35 34 expimpd z 𝒫 ran y z f z z w dom y h = f u | w y u w y h
36 35 ssopab2dv z 𝒫 ran y z f z z w h | w dom y h = f u | w y u w h | w y h
37 opabss w h | w y h y
38 36 37 sstrdi z 𝒫 ran y z f z z w h | w dom y h = f u | w y u y
39 9 38 eqsstrid z 𝒫 ran y z f z z F y
40 27 1 fnmpti F Fn dom y
41 2 ssex F y F V
42 41 adantr F y F Fn dom y F V
43 sseq1 g = F g y F y
44 fneq1 g = F g Fn dom y F Fn dom y
45 43 44 anbi12d g = F g y g Fn dom y F y F Fn dom y
46 45 spcegv F V F y F Fn dom y g g y g Fn dom y
47 42 46 mpcom F y F Fn dom y g g y g Fn dom y
48 39 40 47 sylancl z 𝒫 ran y z f z z g g y g Fn dom y
49 48 exlimiv f z 𝒫 ran y z f z z g g y g Fn dom y
50 7 49 syl x f z x z f z z g g y g Fn dom y
51 sseq1 g = f g y f y
52 fneq1 g = f g Fn dom y f Fn dom y
53 51 52 anbi12d g = f g y g Fn dom y f y f Fn dom y
54 53 cbvexvw g g y g Fn dom y f f y f Fn dom y
55 50 54 sylib x f z x z f z z f f y f Fn dom y