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 \underset{onto}{⟶} B \land Y \in B) \to \exists x \in A F (x) = Y$

Step	Hyp	Ref	Expression
1		forn	$⊢ F : A \underset{onto}{⟶} B \to ran F = B$
2	1	eleq2d	$⊢ F : A \underset{onto}{⟶} B \to (Y \in ran F \leftrightarrow Y \in B)$
3		fofn	$⊢ F : A \underset{onto}{⟶} B \to F Fn A$
4		fvelrnb	$⊢ F Fn A \to (Y \in ran F \leftrightarrow \exists x \in A F (x) = Y)$
5	3 4	syl	$⊢ F : A \underset{onto}{⟶} B \to (Y \in ran F \leftrightarrow \exists x \in A F (x) = Y)$
6	2 5	bitr3d	$⊢ F : A \underset{onto}{⟶} B \to (Y \in B \leftrightarrow \exists x \in A F (x) = Y)$
7	6	biimpa	$⊢ (F : A \underset{onto}{⟶} B \land Y \in B) \to \exists x \in A F (x) = Y$

Metamath Proof Explorer