Theorem 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 \left(F:A\underset{1-1}{⟶}B\wedge \mathrm{ran}F=B\right)$$

Proof

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