f1orn

Description: A one-to-one function maps onto its range. (Contributed by NM, 13-Aug-2004)

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

Step	Hyp	Ref	Expression
1		dff1o2	$⊢ F : A \underset{1-1 onto}{⟶} ran F \leftrightarrow (F Fn A \land Fun F^{-1} \land ran F = ran F)$
2		eqid	$⊢ ran F = ran F$
3		df-3an	$⊢ (F Fn A \land Fun F^{-1} \land ran F = ran F) \leftrightarrow ((F Fn A \land Fun F^{-1}) \land ran F = ran F)$
4	2 3	mpbiran2	$⊢ (F Fn A \land Fun F^{-1} \land ran F = ran F) \leftrightarrow (F Fn A \land Fun F^{-1})$
5	1 4	bitri	$⊢ F : A \underset{1-1 onto}{⟶} ran F \leftrightarrow (F Fn A \land Fun F^{-1})$

Metamath Proof Explorer