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 ) ) )