Metamath Proof Explorer

Theorem imageval

Description: The image functor in maps-to notation. (Contributed by Scott Fenton, 4-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion imageval βŠ’π–¨π—†π–Ίπ—€π–ΎR=x∈V⟼Rx

Proof

Step Hyp Ref Expression
1 funimage ⊒Fun⁑𝖨𝗆𝖺𝗀𝖾R
2 funrel ⊒Fun⁑𝖨𝗆𝖺𝗀𝖾Rβ†’Rel⁑𝖨𝗆𝖺𝗀𝖾R
3 1 2 ax-mp ⊒Rel⁑𝖨𝗆𝖺𝗀𝖾R
4 mptrel ⊒Rel⁑x∈V⟼Rx
5 vex ⊒y∈V
6 vex ⊒z∈V
7 5 6 breldm ⊒y𝖨𝗆𝖺𝗀𝖾Rzβ†’y∈dom⁑𝖨𝗆𝖺𝗀𝖾R
8 fnimage βŠ’π–¨π—†π–Ίπ—€π–ΎRFnx|Rx∈V
9 8 fndmi ⊒dom⁑𝖨𝗆𝖺𝗀𝖾R=x|Rx∈V
10 7 9 eleqtrdi ⊒y𝖨𝗆𝖺𝗀𝖾Rzβ†’y∈x|Rx∈V
11 5 6 breldm ⊒yx∈V⟼Rxzβ†’y∈dom⁑x∈V⟼Rx
12 eqid ⊒x∈V⟼Rx=x∈V⟼Rx
13 12 dmmpt ⊒dom⁑x∈V⟼Rx=x∈V|Rx∈V
14 rabab ⊒x∈V|Rx∈V=x|Rx∈V
15 13 14 eqtri ⊒dom⁑x∈V⟼Rx=x|Rx∈V
16 11 15 eleqtrdi ⊒yx∈V⟼Rxzβ†’y∈x|Rx∈V
17 imaeq2 ⊒x=yβ†’Rx=Ry
18 17 eleq1d ⊒x=yβ†’Rx∈V↔Ry∈V
19 5 18 elab ⊒y∈x|Rx∈V↔Ry∈V
20 5 6 brimage ⊒y𝖨𝗆𝖺𝗀𝖾Rz↔z=Ry
21 eqcom ⊒z=Ry↔Ry=z
22 17 12 fvmptg ⊒y∈V∧Ry∈Vβ†’x∈V⟼Rx⁑y=Ry
23 5 22 mpan ⊒Ry∈Vβ†’x∈V⟼Rx⁑y=Ry
24 23 eqeq1d ⊒Ry∈Vβ†’x∈V⟼Rx⁑y=z↔Ry=z
25 funmpt ⊒Fun⁑x∈V⟼Rx
26 df-fn ⊒x∈V⟼RxFnx|Rx∈V↔Fun⁑x∈V⟼Rx∧dom⁑x∈V⟼Rx=x|Rx∈V
27 25 15 26 mpbir2an ⊒x∈V⟼RxFnx|Rx∈V
28 19 biimpri ⊒Ry∈Vβ†’y∈x|Rx∈V
29 fnbrfvb ⊒x∈V⟼RxFnx|Rx∈V∧y∈x|Rx∈Vβ†’x∈V⟼Rx⁑y=z↔yx∈V⟼Rxz
30 27 28 29 sylancr ⊒Ry∈Vβ†’x∈V⟼Rx⁑y=z↔yx∈V⟼Rxz
31 24 30 bitr3d ⊒Ry∈Vβ†’Ry=z↔yx∈V⟼Rxz
32 21 31 bitrid ⊒Ry∈Vβ†’z=Ry↔yx∈V⟼Rxz
33 20 32 bitrid ⊒Ry∈Vβ†’y𝖨𝗆𝖺𝗀𝖾Rz↔yx∈V⟼Rxz
34 19 33 sylbi ⊒y∈x|Rx∈Vβ†’y𝖨𝗆𝖺𝗀𝖾Rz↔yx∈V⟼Rxz
35 10 16 34 pm5.21nii ⊒y𝖨𝗆𝖺𝗀𝖾Rz↔yx∈V⟼Rxz
36 3 4 35 eqbrriv βŠ’π–¨π—†π–Ίπ—€π–ΎR=x∈V⟼Rx