Theorem f1ocnvb

Description: A relation is a one-to-one onto function iff its converse is a one-to-one onto function with domain and range interchanged. (Contributed by NM, 8-Dec-2003)

	Ref	Expression
Assertion	f1ocnvb	$$⊢\mathrm{Rel}F\to \left(F:A\underset{1-1\; onto}{⟶}B\leftrightarrow F^{-1}:B\underset{1-1\; onto}{⟶}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		f1ocnv	$$⊢F:A\underset{1-1\; onto}{⟶}B\to F^{-1}:B\underset{1-1\; onto}{⟶}A$$
2		f1ocnv	$$⊢F^{-1}:B\underset{1-1\; onto}{⟶}A\to {F^{-1}}^{-1}:A\underset{1-1\; onto}{⟶}B$$
3		dfrel2	$$⊢\mathrm{Rel}F\leftrightarrow {F^{-1}}^{-1}=F$$
4		f1oeq1	$$⊢{F^{-1}}^{-1}=F\to \left({F^{-1}}^{-1}:A\underset{1-1\; onto}{⟶}B\leftrightarrow F:A\underset{1-1\; onto}{⟶}B\right)$$
5	3 4	sylbi	$$⊢\mathrm{Rel}F\to \left({F^{-1}}^{-1}:A\underset{1-1\; onto}{⟶}B\leftrightarrow F:A\underset{1-1\; onto}{⟶}B\right)$$
6	2 5	syl5ib	$$⊢\mathrm{Rel}F\to \left(F^{-1}:B\underset{1-1\; onto}{⟶}A\to F:A\underset{1-1\; onto}{⟶}B\right)$$
7	1 6	impbid2	$$⊢\mathrm{Rel}F\to \left(F:A\underset{1-1\; onto}{⟶}B\leftrightarrow F^{-1}:B\underset{1-1\; onto}{⟶}A\right)$$