Metamath Proof Explorer

Theorem funimage

Description: Image A is a function. (Contributed by Scott Fenton, 27-Mar-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion funimage 
|- Fun Image A

Proof

Step Hyp Ref Expression
1 difss 
 |-  ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E o. `' A ) (x) _V ) ) ) C_ ( _V X. _V )
2 df-rel 
 |-  ( Rel ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E o. `' A ) (x) _V ) ) ) <-> ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E o. `' A ) (x) _V ) ) ) C_ ( _V X. _V ) )
3 1 2 mpbir 
 |-  Rel ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E o. `' A ) (x) _V ) ) )
4 df-image 
 |-  Image A = ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E o. `' A ) (x) _V ) ) )
5 4 releqi 
 |-  ( Rel Image A <-> Rel ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E o. `' A ) (x) _V ) ) ) )
6 3 5 mpbir 
 |-  Rel Image A
7 vex 
 |-  x e. _V
8 vex 
 |-  y e. _V
9 7 8 brimage 
 |-  ( x Image A y <-> y = ( A " x ) )
10 vex 
 |-  z e. _V
11 7 10 brimage 
 |-  ( x Image A z <-> z = ( A " x ) )
12 eqtr3 
 |-  ( ( y = ( A " x ) /\ z = ( A " x ) ) -> y = z )
13 9 11 12 syl2anb 
 |-  ( ( x Image A y /\ x Image A z ) -> y = z )
14 13 gen2 
 |-  A. y A. z ( ( x Image A y /\ x Image A z ) -> y = z )
15 14 ax-gen 
 |-  A. x A. y A. z ( ( x Image A y /\ x Image A z ) -> y = z )
16 dffun2 
 |-  ( Fun Image A <-> ( Rel Image A /\ A. x A. y A. z ( ( x Image A y /\ x Image A z ) -> y = z ) ) )
17 6 15 16 mpbir2an 
 |-  Fun Image A