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 \to (Y \in ran F \to \exists x \in dom F Y = F (x))$

Proof

Step	Hyp	Ref	Expression
1		eqidd	$⊢ Y \in ran F \to Y = Y$
2	1	ancli	$⊢ Y \in ran F \to (Y \in ran F \land Y = Y)$
3	2	adantl	$⊢ (Fun F \land Y \in ran F) \to (Y \in ran F \land Y = Y)$
4		eqeq2	$⊢ y = Y \to (Y = y \leftrightarrow Y = Y)$
5	4	rspcev	$⊢ (Y \in ran F \land Y = Y) \to \exists y \in ran F Y = y$
6	3 5	syl	$⊢ (Fun F \land Y \in ran F) \to \exists y \in ran F Y = y$
7	6	ex	$⊢ Fun F \to (Y \in ran F \to \exists y \in ran F Y = y)$
8		funfn	$⊢ Fun F \leftrightarrow F Fn dom F$
9		eqeq2	$⊢ y = F (x) \to (Y = y \leftrightarrow Y = F (x))$
10	9	rexrn	$⊢ F Fn dom F \to (\exists y \in ran F Y = y \leftrightarrow \exists x \in dom F Y = F (x))$
11	8 10	sylbi	$⊢ Fun F \to (\exists y \in ran F Y = y \leftrightarrow \exists x \in dom F Y = F (x))$
12	7 11	sylibd	$⊢ Fun F \to (Y \in ran F \to \exists x \in dom F Y = F (x))$