Theorem 2fvidf1od

Description: A function is bijective if it has an inverse function. (Contributed by AV, 15-Dec-2019)

	Ref	Expression
Hypotheses	2fvcoidd.f	$$⊢\phi \to F:A⟶B$$
	2fvcoidd.g	$$⊢\phi \to G:B⟶A$$
	2fvcoidd.i	$$⊢\phi \to \forall a\in AG\left(F\left(a\right)\right)=a$$
	2fvidf1od.i	$$⊢\phi \to \forall b\in BF\left(G\left(b\right)\right)=b$$
Assertion	2fvidf1od	$$⊢\phi \to F:A\underset{1-1\; onto}{⟶}B$$

Proof

Step	Hyp	Ref	Expression
1		2fvcoidd.f	$$⊢\phi \to F:A⟶B$$
2		2fvcoidd.g	$$⊢\phi \to G:B⟶A$$
3		2fvcoidd.i	$$⊢\phi \to \forall a\in AG\left(F\left(a\right)\right)=a$$
4		2fvidf1od.i	$$⊢\phi \to \forall b\in BF\left(G\left(b\right)\right)=b$$
5	1 2 3	2fvcoidd	$$⊢\phi \to G\circ F={\mathrm{I}\upharpoonright }_A$$
6	2 1 4	2fvcoidd	$$⊢\phi \to F\circ G={\mathrm{I}\upharpoonright }_B$$
7	1 2 5 6	fcof1od	$$⊢\phi \to F:A\underset{1-1\; onto}{⟶}B$$