Theorem 2fcoidinvd

Description: Show that a function is the inverse of a function if their compositions are the identity functions. (Contributed by Mario Carneiro, 21-Mar-2015) (Revised by AV, 15-Dec-2019)

	Ref	Expression
Hypotheses	fcof1od.f	$$⊢\phi \to F:A⟶B$$
	fcof1od.g	$$⊢\phi \to G:B⟶A$$
	fcof1od.a	$$⊢\phi \to G\circ F={\mathrm{I}\upharpoonright }_A$$
	fcof1od.b	$$⊢\phi \to F\circ G={\mathrm{I}\upharpoonright }_B$$
Assertion	2fcoidinvd	$$⊢\phi \to F^{-1}=G$$

Proof

Step	Hyp	Ref	Expression
1		fcof1od.f	$$⊢\phi \to F:A⟶B$$
2		fcof1od.g	$$⊢\phi \to G:B⟶A$$
3		fcof1od.a	$$⊢\phi \to G\circ F={\mathrm{I}\upharpoonright }_A$$
4		fcof1od.b	$$⊢\phi \to F\circ G={\mathrm{I}\upharpoonright }_B$$
5	1 2 3 4	fcof1od	$$⊢\phi \to F:A\underset{1-1\; onto}{⟶}B$$
6	5 2 4	fcof1oinvd	$$⊢\phi \to F^{-1}=G$$