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		f1f	$⊢ F : A \underset{1-1}{⟶} B \to F : A ⟶ B$
3	2	biantrurd	$⊢ F : A \underset{1-1}{⟶} B \to (ran F = B \leftrightarrow (F : A ⟶ B \land ran F = B))$
4		dffo2	$⊢ F : A \underset{onto}{⟶} B \leftrightarrow (F : A ⟶ B \land ran F = B)$
5	3 4	syl6rbbr	$⊢ 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