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 R x

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 R x
5 vex y V
6 vex z V
7 5 6 breldm y 𝖨𝗆𝖺𝗀𝖾 R z y dom 𝖨𝗆𝖺𝗀𝖾 R
8 fnimage 𝖨𝗆𝖺𝗀𝖾 R Fn x | R x V
9 8 fndmi dom 𝖨𝗆𝖺𝗀𝖾 R = x | R x V
10 7 9 eleqtrdi y 𝖨𝗆𝖺𝗀𝖾 R z y x | R x V
11 5 6 breldm y x V R x z y dom x V R x
12 eqid x V R x = x V R x
13 12 dmmpt dom x V R x = x V | R x V
14 rabab x V | R x V = x | R x V
15 13 14 eqtri dom x V R x = x | R x V
16 11 15 eleqtrdi y x V R x z y x | R x V
17 imaeq2 x = y R x = R y
18 17 eleq1d x = y R x V R y V
19 5 18 elab y x | R x V R y V
20 5 6 brimage y 𝖨𝗆𝖺𝗀𝖾 R z z = R y
21 eqcom z = R y R y = z
22 17 12 fvmptg y V R y V x V R x y = R y
23 5 22 mpan R y V x V R x y = R y
24 23 eqeq1d R y V x V R x y = z R y = z
25 funmpt Fun x V R x
26 df-fn x V R x Fn x | R x V Fun x V R x dom x V R x = x | R x V
27 25 15 26 mpbir2an x V R x Fn x | R x V
28 19 biimpri R y V y x | R x V
29 fnbrfvb x V R x Fn x | R x V y x | R x V x V R x y = z y x V R x z
30 27 28 29 sylancr R y V x V R x y = z y x V R x z
31 24 30 bitr3d R y V R y = z y x V R x z
32 21 31 syl5bb R y V z = R y y x V R x z
33 20 32 syl5bb R y V y 𝖨𝗆𝖺𝗀𝖾 R z y x V R x z
34 19 33 sylbi y x | R x V y 𝖨𝗆𝖺𝗀𝖾 R z y x V R x z
35 10 16 34 pm5.21nii y 𝖨𝗆𝖺𝗀𝖾 R z y x V R x z
36 3 4 35 eqbrriv 𝖨𝗆𝖺𝗀𝖾 R = x V R x