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	⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		forn	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ran 𝐹 = 𝐵 )
2	1	eleq2d	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( 𝑌 ∈ ran 𝐹 ↔ 𝑌 ∈ 𝐵 ) )
3		fofn	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐹 Fn 𝐴 )
4		fvelrnb	⊢ ( 𝐹 Fn 𝐴 → ( 𝑌 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑌 ) )
5	3 4	syl	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( 𝑌 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑌 ) )
6	2 5	bitr3d	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( 𝑌 ∈ 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑌 ) )
7	6	biimpa	⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑌 )