Metamath Proof Explorer

Theorem f11o

Description: Relationship between one-to-one and one-to-one onto function. (Contributed by NM, 4-Apr-1998)

		Ref	Expression
	Hypothesis	f11o.1	$⊢ F \in V$
	Assertion	f11o	$⊢ F : A \underset{1-1}{⟶} B \leftrightarrow \exists x (F : A \underset{1-1 onto}{⟶} x \land x \subseteq B)$

Proof

Step	Hyp	Ref	Expression
1		f11o.1	$⊢ F \in V$
2	1	ffoss	$⊢ F : A ⟶ B \leftrightarrow \exists x (F : A \underset{onto}{⟶} x \land x \subseteq B)$
3	2	anbi1i	$⊢ (F : A ⟶ B \land Fun F^{-1}) \leftrightarrow (\exists x (F : A \underset{onto}{⟶} x \land x \subseteq B) \land Fun F^{-1})$
4		df-f1	$⊢ F : A \underset{1-1}{⟶} B \leftrightarrow (F : A ⟶ B \land Fun F^{-1})$
5		dff1o3	$⊢ F : A \underset{1-1 onto}{⟶} x \leftrightarrow (F : A \underset{onto}{⟶} x \land Fun F^{-1})$
6	5	anbi1i	$⊢ (F : A \underset{1-1 onto}{⟶} x \land x \subseteq B) \leftrightarrow ((F : A \underset{onto}{⟶} x \land Fun F^{-1}) \land x \subseteq B)$
7		an32	$⊢ ((F : A \underset{onto}{⟶} x \land Fun F^{-1}) \land x \subseteq B) \leftrightarrow ((F : A \underset{onto}{⟶} x \land x \subseteq B) \land Fun F^{-1})$
8	6 7	bitri	$⊢ (F : A \underset{1-1 onto}{⟶} x \land x \subseteq B) \leftrightarrow ((F : A \underset{onto}{⟶} x \land x \subseteq B) \land Fun F^{-1})$
9	8	exbii	$⊢ \exists x (F : A \underset{1-1 onto}{⟶} x \land x \subseteq B) \leftrightarrow \exists x ((F : A \underset{onto}{⟶} x \land x \subseteq B) \land Fun F^{-1})$
10		19.41v	$⊢ \exists x ((F : A \underset{onto}{⟶} x \land x \subseteq B) \land Fun F^{-1}) \leftrightarrow (\exists x (F : A \underset{onto}{⟶} x \land x \subseteq B) \land Fun F^{-1})$
11	9 10	bitri	$⊢ \exists x (F : A \underset{1-1 onto}{⟶} x \land x \subseteq B) \leftrightarrow (\exists x (F : A \underset{onto}{⟶} x \land x \subseteq B) \land Fun F^{-1})$
12	3 4 11	3bitr4i	$⊢ F : A \underset{1-1}{⟶} B \leftrightarrow \exists x (F : A \underset{1-1 onto}{⟶} x \land x \subseteq B)$