Theorem foelcdmi

Description: A member of a surjective function's codomain is a value of the function. (Contributed by Thierry Arnoux, 23-Jan-2020)

	Ref	Expression
Assertion	foelcdmi	|- ( ( F : A -onto-> B /\ Y e. B ) -> E. x e. A ( F ` x ) = Y )

Proof

Step	Hyp	Ref	Expression
1		forn	|- ( F : A -onto-> B -> ran F = B )
2	1	eleq2d	|- ( F : A -onto-> B -> ( Y e. ran F <-> Y e. B ) )
3		fofn	|- ( F : A -onto-> B -> F Fn A )
4		fvelrnb	|- ( F Fn A -> ( Y e. ran F <-> E. x e. A ( F ` x ) = Y ) )
5	3 4	syl	|- ( F : A -onto-> B -> ( Y e. ran F <-> E. x e. A ( F ` x ) = Y ) )
6	2 5	bitr3d	|- ( F : A -onto-> B -> ( Y e. B <-> E. x e. A ( F ` x ) = Y ) )
7	6	biimpa	|- ( ( F : A -onto-> B /\ Y e. B ) -> E. x e. A ( F ` x ) = Y )