Theorem fcof1oinvd

Description: Show that a function is the inverse of a bijective function if their composition is the identity function. Formerly part of proof of fcof1o . (Contributed by Mario Carneiro, 21-Mar-2015) (Revised by AV, 15-Dec-2019)

	Ref	Expression
Hypotheses	fcof1oinvd.f	$$⊢\phi \to F:A\underset{1-1\; onto}{⟶}B$$
	fcof1oinvd.g	$$⊢\phi \to G:B⟶A$$
	fcof1oinvd.b	$$⊢\phi \to F\circ G={\mathrm{I}\upharpoonright }_B$$
Assertion	fcof1oinvd	$$⊢\phi \to F^{-1}=G$$

Proof

Step	Hyp	Ref	Expression
1		fcof1oinvd.f	$$⊢\phi \to F:A\underset{1-1\; onto}{⟶}B$$
2		fcof1oinvd.g	$$⊢\phi \to G:B⟶A$$
3		fcof1oinvd.b	$$⊢\phi \to F\circ G={\mathrm{I}\upharpoonright }_B$$
4	3	coeq2d	$$⊢\phi \to F^{-1}\circ \left(F\circ G\right)=F^{-1}\circ \left({\mathrm{I}\upharpoonright }_B\right)$$
5		coass	$$⊢\left(F^{-1}\circ F\right)\circ G=F^{-1}\circ \left(F\circ G\right)$$
6		f1ococnv1	$$⊢F:A\underset{1-1\; onto}{⟶}B\to F^{-1}\circ F={\mathrm{I}\upharpoonright }_A$$
7	1 6	syl	$$⊢\phi \to F^{-1}\circ F={\mathrm{I}\upharpoonright }_A$$
8	7	coeq1d	$$⊢\phi \to \left(F^{-1}\circ F\right)\circ G=\left({\mathrm{I}\upharpoonright }_A\right)\circ G$$
9		fcoi2	$$⊢G:B⟶A\to \left({\mathrm{I}\upharpoonright }_A\right)\circ G=G$$
10	2 9	syl	$$⊢\phi \to \left({\mathrm{I}\upharpoonright }_A\right)\circ G=G$$
11	8 10	eqtrd	$$⊢\phi \to \left(F^{-1}\circ F\right)\circ G=G$$
12	5 11	syl5eqr	$$⊢\phi \to F^{-1}\circ \left(F\circ G\right)=G$$
13		f1ocnv	$$⊢F:A\underset{1-1\; onto}{⟶}B\to F^{-1}:B\underset{1-1\; onto}{⟶}A$$
14	1 13	syl	$$⊢\phi \to F^{-1}:B\underset{1-1\; onto}{⟶}A$$
15		f1of	$$⊢F^{-1}:B\underset{1-1\; onto}{⟶}A\to F^{-1}:B⟶A$$
16	14 15	syl	$$⊢\phi \to F^{-1}:B⟶A$$
17		fcoi1	$$⊢F^{-1}:B⟶A\to F^{-1}\circ \left({\mathrm{I}\upharpoonright }_B\right)=F^{-1}$$
18	16 17	syl	$$⊢\phi \to F^{-1}\circ \left({\mathrm{I}\upharpoonright }_B\right)=F^{-1}$$
19	4 12 18	3eqtr3rd	$$⊢\phi \to F^{-1}=G$$