Metamath Proof Explorer


Theorem fvrnressn

Description: If the value of a function is in the range of the function restricted to the singleton containing the argument, then the value of the function is in the range of the function. (Contributed by Alexander van der Vekens, 22-Jul-2018)

Ref Expression
Assertion fvrnressn
|- ( X e. V -> ( ( F ` X ) e. ran ( F |` { X } ) -> ( F ` X ) e. ran F ) )

Proof

Step Hyp Ref Expression
1 df-ima
 |-  ( F " { X } ) = ran ( F |` { X } )
2 1 eleq2i
 |-  ( ( F ` X ) e. ( F " { X } ) <-> ( F ` X ) e. ran ( F |` { X } ) )
3 opeq1
 |-  ( x = X -> <. x , ( F ` X ) >. = <. X , ( F ` X ) >. )
4 3 eleq1d
 |-  ( x = X -> ( <. x , ( F ` X ) >. e. F <-> <. X , ( F ` X ) >. e. F ) )
5 4 spcegv
 |-  ( X e. V -> ( <. X , ( F ` X ) >. e. F -> E. x <. x , ( F ` X ) >. e. F ) )
6 fvex
 |-  ( F ` X ) e. _V
7 elimasng
 |-  ( ( X e. V /\ ( F ` X ) e. _V ) -> ( ( F ` X ) e. ( F " { X } ) <-> <. X , ( F ` X ) >. e. F ) )
8 6 7 mpan2
 |-  ( X e. V -> ( ( F ` X ) e. ( F " { X } ) <-> <. X , ( F ` X ) >. e. F ) )
9 elrn2g
 |-  ( ( F ` X ) e. _V -> ( ( F ` X ) e. ran F <-> E. x <. x , ( F ` X ) >. e. F ) )
10 6 9 mp1i
 |-  ( X e. V -> ( ( F ` X ) e. ran F <-> E. x <. x , ( F ` X ) >. e. F ) )
11 5 8 10 3imtr4d
 |-  ( X e. V -> ( ( F ` X ) e. ( F " { X } ) -> ( F ` X ) e. ran F ) )
12 2 11 syl5bir
 |-  ( X e. V -> ( ( F ` X ) e. ran ( F |` { X } ) -> ( F ` X ) e. ran F ) )