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 
|- Image R = ( x e. _V |-> ( R " x ) )

Proof

Step Hyp Ref Expression
1 funimage 
 |-  Fun Image R
2 funrel 
 |-  ( Fun Image R -> Rel Image R )
3 1 2 ax-mp 
 |-  Rel Image R
4 mptrel 
 |-  Rel ( x e. _V |-> ( R " x ) )
5 vex 
 |-  y e. _V
6 vex 
 |-  z e. _V
7 5 6 breldm 
 |-  ( y Image R z -> y e. dom Image R )
8 fnimage 
 |-  Image R Fn { x | ( R " x ) e. _V }
9 8 fndmi 
 |-  dom Image R = { x | ( R " x ) e. _V }
10 7 9 eleqtrdi 
 |-  ( y Image R z -> y e. { x | ( R " x ) e. _V } )
11 5 6 breldm 
 |-  ( y ( x e. _V |-> ( R " x ) ) z -> y e. dom ( x e. _V |-> ( R " x ) ) )
12 eqid 
 |-  ( x e. _V |-> ( R " x ) ) = ( x e. _V |-> ( R " x ) )
13 12 dmmpt 
 |-  dom ( x e. _V |-> ( R " x ) ) = { x e. _V | ( R " x ) e. _V }
14 rabab 
 |-  { x e. _V | ( R " x ) e. _V } = { x | ( R " x ) e. _V }
15 13 14 eqtri 
 |-  dom ( x e. _V |-> ( R " x ) ) = { x | ( R " x ) e. _V }
16 11 15 eleqtrdi 
 |-  ( y ( x e. _V |-> ( R " x ) ) z -> y e. { x | ( R " x ) e. _V } )
17 imaeq2 
 |-  ( x = y -> ( R " x ) = ( R " y ) )
18 17 eleq1d 
 |-  ( x = y -> ( ( R " x ) e. _V <-> ( R " y ) e. _V ) )
19 5 18 elab 
 |-  ( y e. { x | ( R " x ) e. _V } <-> ( R " y ) e. _V )
20 5 6 brimage 
 |-  ( y Image R z <-> z = ( R " y ) )
21 eqcom 
 |-  ( z = ( R " y ) <-> ( R " y ) = z )
22 17 12 fvmptg 
 |-  ( ( y e. _V /\ ( R " y ) e. _V ) -> ( ( x e. _V |-> ( R " x ) ) ` y ) = ( R " y ) )
23 5 22 mpan 
 |-  ( ( R " y ) e. _V -> ( ( x e. _V |-> ( R " x ) ) ` y ) = ( R " y ) )
24 23 eqeq1d 
 |-  ( ( R " y ) e. _V -> ( ( ( x e. _V |-> ( R " x ) ) ` y ) = z <-> ( R " y ) = z ) )
25 funmpt 
 |-  Fun ( x e. _V |-> ( R " x ) )
26 df-fn 
 |-  ( ( x e. _V |-> ( R " x ) ) Fn { x | ( R " x ) e. _V } <-> ( Fun ( x e. _V |-> ( R " x ) ) /\ dom ( x e. _V |-> ( R " x ) ) = { x | ( R " x ) e. _V } ) )
27 25 15 26 mpbir2an 
 |-  ( x e. _V |-> ( R " x ) ) Fn { x | ( R " x ) e. _V }
28 19 biimpri 
 |-  ( ( R " y ) e. _V -> y e. { x | ( R " x ) e. _V } )
29 fnbrfvb 
 |-  ( ( ( x e. _V |-> ( R " x ) ) Fn { x | ( R " x ) e. _V } /\ y e. { x | ( R " x ) e. _V } ) -> ( ( ( x e. _V |-> ( R " x ) ) ` y ) = z <-> y ( x e. _V |-> ( R " x ) ) z ) )
30 27 28 29 sylancr 
 |-  ( ( R " y ) e. _V -> ( ( ( x e. _V |-> ( R " x ) ) ` y ) = z <-> y ( x e. _V |-> ( R " x ) ) z ) )
31 24 30 bitr3d 
 |-  ( ( R " y ) e. _V -> ( ( R " y ) = z <-> y ( x e. _V |-> ( R " x ) ) z ) )
32 21 31 syl5bb 
 |-  ( ( R " y ) e. _V -> ( z = ( R " y ) <-> y ( x e. _V |-> ( R " x ) ) z ) )
33 20 32 syl5bb 
 |-  ( ( R " y ) e. _V -> ( y Image R z <-> y ( x e. _V |-> ( R " x ) ) z ) )
34 19 33 sylbi 
 |-  ( y e. { x | ( R " x ) e. _V } -> ( y Image R z <-> y ( x e. _V |-> ( R " x ) ) z ) )
35 10 16 34 pm5.21nii 
 |-  ( y Image R z <-> y ( x e. _V |-> ( R " x ) ) z )
36 3 4 35 eqbrriv 
 |-  Image R = ( x e. _V |-> ( R " x ) )