Metamath Proof Explorer

Theorem dff1o6

Description: A one-to-one onto function in terms of function values. (Contributed by NM, 29-Mar-2008)

		Ref	Expression
	Assertion	dff1o6	$⊢ F : A \underset{1-1 onto}{⟶} B \leftrightarrow (F Fn A \land ran F = B \land \forall x \in A \forall y \in A (F (x) = F (y) \to x = y))$

Proof

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		dff13	$⊢ F : A \underset{1-1}{⟶} B \leftrightarrow (F : A ⟶ B \land \forall x \in A \forall y \in A (F (x) = F (y) \to x = y))$
3		df-fo	$⊢ F : A \underset{onto}{⟶} B \leftrightarrow (F Fn A \land ran F = B)$
4	2 3	anbi12i	$⊢ (F : A \underset{1-1}{⟶} B \land F : A \underset{onto}{⟶} B) \leftrightarrow ((F : A ⟶ B \land \forall x \in A \forall y \in A (F (x) = F (y) \to x = y)) \land (F Fn A \land ran F = B))$
5		df-3an	$⊢ (F Fn A \land ran F = B \land \forall x \in A \forall y \in A (F (x) = F (y) \to x = y)) \leftrightarrow ((F Fn A \land ran F = B) \land \forall x \in A \forall y \in A (F (x) = F (y) \to x = y))$
6		eqimss	$⊢ ran F = B \to ran F \subseteq B$
7	6	anim2i	$⊢ (F Fn A \land ran F = B) \to (F Fn A \land ran F \subseteq B)$
8		df-f	$⊢ F : A ⟶ B \leftrightarrow (F Fn A \land ran F \subseteq B)$
9	7 8	sylibr	$⊢ (F Fn A \land ran F = B) \to F : A ⟶ B$
10	9	pm4.71ri	$⊢ (F Fn A \land ran F = B) \leftrightarrow (F : A ⟶ B \land (F Fn A \land ran F = B))$
11	10	anbi1i	$⊢ ((F Fn A \land ran F = B) \land \forall x \in A \forall y \in A (F (x) = F (y) \to x = y)) \leftrightarrow ((F : A ⟶ B \land (F Fn A \land ran F = B)) \land \forall x \in A \forall y \in A (F (x) = F (y) \to x = y))$
12		an32	$⊢ ((F : A ⟶ B \land (F Fn A \land ran F = B)) \land \forall x \in A \forall y \in A (F (x) = F (y) \to x = y)) \leftrightarrow ((F : A ⟶ B \land \forall x \in A \forall y \in A (F (x) = F (y) \to x = y)) \land (F Fn A \land ran F = B))$
13	5 11 12	3bitrri	$⊢ ((F : A ⟶ B \land \forall x \in A \forall y \in A (F (x) = F (y) \to x = y)) \land (F Fn A \land ran F = B)) \leftrightarrow (F Fn A \land ran F = B \land \forall x \in A \forall y \in A (F (x) = F (y) \to x = y))$
14	1 4 13	3bitri	$⊢ F : A \underset{1-1 onto}{⟶} B \leftrightarrow (F Fn A \land ran F = B \land \forall x \in A \forall y \in A (F (x) = F (y) \to x = y))$