Theorem foelrnf

Description: Property of a surjective function. As foelrn but with less disjoint vars constraints. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypothesis	foelrnf.1	⊢ Ⅎ 𝑥 𝐹
Assertion	foelrnf	⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐶 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝐶 = ( 𝐹 ‘ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		foelrnf.1	⊢ Ⅎ 𝑥 𝐹
2	1	dffo3f	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
3	2	simprbi	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) )
4		eqeq1	⊢ ( 𝑦 = 𝐶 → ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ 𝐶 = ( 𝐹 ‘ 𝑥 ) ) )
5	4	rexbidv	⊢ ( 𝑦 = 𝐶 → ( ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐴 𝐶 = ( 𝐹 ‘ 𝑥 ) ) )
6	5	rspccva	⊢ ( ( ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ∧ 𝐶 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝐶 = ( 𝐹 ‘ 𝑥 ) )
7	3 6	sylan	⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐶 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝐶 = ( 𝐹 ‘ 𝑥 ) )