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 𝐹 → ( 𝑌 ∈ ran 𝐹 → ∃ 𝑥 ∈ dom 𝐹 𝑌 = ( 𝐹 ‘ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqidd	⊢ ( 𝑌 ∈ ran 𝐹 → 𝑌 = 𝑌 )
2	1	ancli	⊢ ( 𝑌 ∈ ran 𝐹 → ( 𝑌 ∈ ran 𝐹 ∧ 𝑌 = 𝑌 ) )
3	2	adantl	⊢ ( ( Fun 𝐹 ∧ 𝑌 ∈ ran 𝐹 ) → ( 𝑌 ∈ ran 𝐹 ∧ 𝑌 = 𝑌 ) )
4		eqeq2	⊢ ( 𝑦 = 𝑌 → ( 𝑌 = 𝑦 ↔ 𝑌 = 𝑌 ) )
5	4	rspcev	⊢ ( ( 𝑌 ∈ ran 𝐹 ∧ 𝑌 = 𝑌 ) → ∃ 𝑦 ∈ ran 𝐹 𝑌 = 𝑦 )
6	3 5	syl	⊢ ( ( Fun 𝐹 ∧ 𝑌 ∈ ran 𝐹 ) → ∃ 𝑦 ∈ ran 𝐹 𝑌 = 𝑦 )
7	6	ex	⊢ ( Fun 𝐹 → ( 𝑌 ∈ ran 𝐹 → ∃ 𝑦 ∈ ran 𝐹 𝑌 = 𝑦 ) )
8		funfn	⊢ ( Fun 𝐹 ↔ 𝐹 Fn dom 𝐹 )
9		eqeq2	⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( 𝑌 = 𝑦 ↔ 𝑌 = ( 𝐹 ‘ 𝑥 ) ) )
10	9	rexrn	⊢ ( 𝐹 Fn dom 𝐹 → ( ∃ 𝑦 ∈ ran 𝐹 𝑌 = 𝑦 ↔ ∃ 𝑥 ∈ dom 𝐹 𝑌 = ( 𝐹 ‘ 𝑥 ) ) )
11	8 10	sylbi	⊢ ( Fun 𝐹 → ( ∃ 𝑦 ∈ ran 𝐹 𝑌 = 𝑦 ↔ ∃ 𝑥 ∈ dom 𝐹 𝑌 = ( 𝐹 ‘ 𝑥 ) ) )
12	7 11	sylibd	⊢ ( Fun 𝐹 → ( 𝑌 ∈ ran 𝐹 → ∃ 𝑥 ∈ dom 𝐹 𝑌 = ( 𝐹 ‘ 𝑥 ) ) )