dff1o3

Description: Alternate definition of one-to-one onto function. (Contributed by NM, 25-Mar-1998) (Proof shortened by Andrew Salmon, 22-Oct-2011)

		Ref	Expression
	Assertion	dff1o3	$⊢ F : A \underset{1-1 onto}{⟶} B \leftrightarrow (F : A \underset{onto}{⟶} B \land Fun F^{-1})$

Step	Hyp	Ref	Expression
1		3anan32	$⊢ (F Fn A \land Fun F^{-1} \land ran F = B) \leftrightarrow ((F Fn A \land ran F = B) \land Fun F^{-1})$
2		dff1o2	$⊢ F : A \underset{1-1 onto}{⟶} B \leftrightarrow (F Fn A \land Fun F^{-1} \land ran F = B)$
3		df-fo	$⊢ F : A \underset{onto}{⟶} B \leftrightarrow (F Fn A \land ran F = B)$
4	3	anbi1i	$⊢ (F : A \underset{onto}{⟶} B \land Fun F^{-1}) \leftrightarrow ((F Fn A \land ran F = B) \land Fun F^{-1})$
5	1 2 4	3bitr4i	$⊢ F : A \underset{1-1 onto}{⟶} B \leftrightarrow (F : A \underset{onto}{⟶} B \land Fun F^{-1})$

Metamath Proof Explorer