This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fnimage

Description: Image R is a function over the set-like portion of R . (Contributed by Scott Fenton, 4-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion fnimage 
|- Image R Fn { x | ( R " x ) e. _V }

Proof

Step Hyp Ref Expression
1 funimage 
 |-  Fun Image R
2 vex 
 |-  y e. _V
3 vex 
 |-  x e. _V
4 2 3 brimage 
 |-  ( y Image R x <-> x = ( R " y ) )
5 eqvisset 
 |-  ( x = ( R " y ) -> ( R " y ) e. _V )
6 4 5 sylbi 
 |-  ( y Image R x -> ( R " y ) e. _V )
7 6 exlimiv 
 |-  ( E. x y Image R x -> ( R " y ) e. _V )
8 eqid 
 |-  ( R " y ) = ( R " y )
9 brimageg 
 |-  ( ( y e. _V /\ ( R " y ) e. _V ) -> ( y Image R ( R " y ) <-> ( R " y ) = ( R " y ) ) )
10 2 9 mpan 
 |-  ( ( R " y ) e. _V -> ( y Image R ( R " y ) <-> ( R " y ) = ( R " y ) ) )
11 8 10 mpbiri 
 |-  ( ( R " y ) e. _V -> y Image R ( R " y ) )
12 breq2 
 |-  ( x = ( R " y ) -> ( y Image R x <-> y Image R ( R " y ) ) )
13 12 spcegv 
 |-  ( ( R " y ) e. _V -> ( y Image R ( R " y ) -> E. x y Image R x ) )
14 11 13 mpd 
 |-  ( ( R " y ) e. _V -> E. x y Image R x )
15 7 14 impbii 
 |-  ( E. x y Image R x <-> ( R " y ) e. _V )
16 2 eldm 
 |-  ( y e. dom Image R <-> E. x y Image R x )
17 imaeq2 
 |-  ( x = y -> ( R " x ) = ( R " y ) )
18 17 eleq1d 
 |-  ( x = y -> ( ( R " x ) e. _V <-> ( R " y ) e. _V ) )
19 2 18 elab 
 |-  ( y e. { x | ( R " x ) e. _V } <-> ( R " y ) e. _V )
20 15 16 19 3bitr4i 
 |-  ( y e. dom Image R <-> y e. { x | ( R " x ) e. _V } )
21 20 eqriv 
 |-  dom Image R = { x | ( R " x ) e. _V }
22 df-fn 
 |-  ( Image R Fn { x | ( R " x ) e. _V } <-> ( Fun Image R /\ dom Image R = { x | ( R " x ) e. _V } ) )
23 1 21 22 mpbir2an 
 |-  Image R Fn { x | ( R " x ) e. _V }