Theorem dffo2

Description: Alternate definition of an onto function. (Contributed by NM, 22-Mar-2006)

	Ref	Expression
Assertion	dffo2	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ran 𝐹 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		fof	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
2		forn	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ran 𝐹 = 𝐵 )
3	1 2	jca	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ran 𝐹 = 𝐵 ) )
4		ffn	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
5		df-fo	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵 ) )
6	5	biimpri	⊢ ( ( 𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵 ) → 𝐹 : 𝐴 –onto→ 𝐵 )
7	4 6	sylan	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ran 𝐹 = 𝐵 ) → 𝐹 : 𝐴 –onto→ 𝐵 )
8	3 7	impbii	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ran 𝐹 = 𝐵 ) )