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

Metamath Proof Explorer

Theorem elrnrexdm

Description: For any element in the range of a function there is an element in the domain of the function for which the function value is the element of the range. (Contributed by Alexander van der Vekens, 8-Dec-2017)

Ref Expression
Assertion elrnrexdm 
|- ( Fun F -> ( Y e. ran F -> E. x e. dom F Y = ( F ` x ) ) )

Proof

Step Hyp Ref Expression
1 eqidd 
 |-  ( Y e. ran F -> Y = Y )
2 1 ancli 
 |-  ( Y e. ran F -> ( Y e. ran F /\ Y = Y ) )
3 2 adantl 
 |-  ( ( Fun F /\ Y e. ran F ) -> ( Y e. ran F /\ Y = Y ) )
4 eqeq2 
 |-  ( y = Y -> ( Y = y <-> Y = Y ) )
5 4 rspcev 
 |-  ( ( Y e. ran F /\ Y = Y ) -> E. y e. ran F Y = y )
6 3 5 syl 
 |-  ( ( Fun F /\ Y e. ran F ) -> E. y e. ran F Y = y )
7 6 ex 
 |-  ( Fun F -> ( Y e. ran F -> E. y e. ran F Y = y ) )
8 funfn 
 |-  ( Fun F <-> F Fn dom F )
9 eqeq2 
 |-  ( y = ( F ` x ) -> ( Y = y <-> Y = ( F ` x ) ) )
10 9 rexrn 
 |-  ( F Fn dom F -> ( E. y e. ran F Y = y <-> E. x e. dom F Y = ( F ` x ) ) )
11 8 10 sylbi 
 |-  ( Fun F -> ( E. y e. ran F Y = y <-> E. x e. dom F Y = ( F ` x ) ) )
12 7 11 sylibd 
 |-  ( Fun F -> ( Y e. ran F -> E. x e. dom F Y = ( F ` x ) ) )