Theorem foelrn

Description: Property of a surjective function. (Contributed by Jeff Madsen, 4-Jan-2011)

	Ref	Expression
Assertion	foelrn	⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐶 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝐶 = ( 𝐹 ‘ 𝑥 ) )

Proof

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