Theorem f1oexbi

Description: There is a one-to-one onto function from a set to a second set iff there is a one-to-one onto function from the second set to the first set. (Contributed by Alexander van der Vekens, 30-Sep-2018)

	Ref	Expression
Assertion	f1oexbi	$$⊢\exists ff:A\underset{1-1\; onto}{⟶}B\leftrightarrow \exists gg:B\underset{1-1\; onto}{⟶}A$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢f\in \mathrm{V}$$
2	1	cnvex	$$⊢f^{-1}\in \mathrm{V}$$
3		f1ocnv	$$⊢f:A\underset{1-1\; onto}{⟶}B\to f^{-1}:B\underset{1-1\; onto}{⟶}A$$
4		f1oeq1	$$⊢g=f^{-1}\to \left(g:B\underset{1-1\; onto}{⟶}A\leftrightarrow f^{-1}:B\underset{1-1\; onto}{⟶}A\right)$$
5	4	spcegv	$$⊢f^{-1}\in \mathrm{V}\to \left(f^{-1}:B\underset{1-1\; onto}{⟶}A\to \exists gg:B\underset{1-1\; onto}{⟶}A\right)$$
6	2 3 5	mpsyl	$$⊢f:A\underset{1-1\; onto}{⟶}B\to \exists gg:B\underset{1-1\; onto}{⟶}A$$
7	6	exlimiv	$$⊢\exists ff:A\underset{1-1\; onto}{⟶}B\to \exists gg:B\underset{1-1\; onto}{⟶}A$$
8		vex	$$⊢g\in \mathrm{V}$$
9	8	cnvex	$$⊢g^{-1}\in \mathrm{V}$$
10		f1ocnv	$$⊢g:B\underset{1-1\; onto}{⟶}A\to g^{-1}:A\underset{1-1\; onto}{⟶}B$$
11		f1oeq1	$$⊢f=g^{-1}\to \left(f:A\underset{1-1\; onto}{⟶}B\leftrightarrow g^{-1}:A\underset{1-1\; onto}{⟶}B\right)$$
12	11	spcegv	$$⊢g^{-1}\in \mathrm{V}\to \left(g^{-1}:A\underset{1-1\; onto}{⟶}B\to \exists ff:A\underset{1-1\; onto}{⟶}B\right)$$
13	9 10 12	mpsyl	$$⊢g:B\underset{1-1\; onto}{⟶}A\to \exists ff:A\underset{1-1\; onto}{⟶}B$$
14	13	exlimiv	$$⊢\exists gg:B\underset{1-1\; onto}{⟶}A\to \exists ff:A\underset{1-1\; onto}{⟶}B$$
15	7 14	impbii	$$⊢\exists ff:A\underset{1-1\; onto}{⟶}B\leftrightarrow \exists gg:B\underset{1-1\; onto}{⟶}A$$