dffo2

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

		Ref	Expression
	Assertion	dffo2	$⊢ F : A \underset{onto}{⟶} B \leftrightarrow (F : A ⟶ B \land ran F = B)$

Step	Hyp	Ref	Expression
1		fof	$⊢ F : A \underset{onto}{⟶} B \to F : A ⟶ B$
2		forn	$⊢ F : A \underset{onto}{⟶} B \to ran F = B$
3	1 2	jca	$⊢ F : A \underset{onto}{⟶} B \to (F : A ⟶ B \land ran F = B)$
4		ffn	$⊢ F : A ⟶ B \to F Fn A$
5		df-fo	$⊢ F : A \underset{onto}{⟶} B \leftrightarrow (F Fn A \land ran F = B)$
6	5	biimpri	$⊢ (F Fn A \land ran F = B) \to F : A \underset{onto}{⟶} B$
7	4 6	sylan	$⊢ (F : A ⟶ B \land ran F = B) \to F : A \underset{onto}{⟶} B$
8	3 7	impbii	$⊢ F : A \underset{onto}{⟶} B \leftrightarrow (F : A ⟶ B \land ran F = B)$

Metamath Proof Explorer