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 }