dff1o5

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

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

Step	Hyp	Ref	Expression
1		df-f1o	$⊢ F : A \underset{1-1 onto}{⟶} B \leftrightarrow (F : A \underset{1-1}{⟶} B \land F : A \underset{onto}{⟶} B)$
2		dffo2	$⊢ F : A \underset{onto}{⟶} B \leftrightarrow (F : A ⟶ B \land ran F = B)$
3		f1f	$⊢ F : A \underset{1-1}{⟶} B \to F : A ⟶ B$
4	3	biantrurd	$⊢ F : A \underset{1-1}{⟶} B \to (ran F = B \leftrightarrow (F : A ⟶ B \land ran F = B))$
5	2 4	bitr4id	$⊢ F : A \underset{1-1}{⟶} B \to (F : A \underset{onto}{⟶} B \leftrightarrow ran F = B)$
6	5	pm5.32i	$⊢ (F : A \underset{1-1}{⟶} B \land F : A \underset{onto}{⟶} B) \leftrightarrow (F : A \underset{1-1}{⟶} B \land ran F = B)$
7	1 6	bitri	$⊢ F : A \underset{1-1 onto}{⟶} B \leftrightarrow (F : A \underset{1-1}{⟶} B \land ran F = B)$

Metamath Proof Explorer