Metamath Proof Explorer


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 φ F : A 1-1 onto B
fcof1oinvd.g φ G : B A
fcof1oinvd.b φ F G = I B
Assertion fcof1oinvd φ F -1 = G

Proof

Step Hyp Ref Expression
1 fcof1oinvd.f φ F : A 1-1 onto B
2 fcof1oinvd.g φ G : B A
3 fcof1oinvd.b φ F G = I B
4 3 coeq2d φ F -1 F G = F -1 I B
5 coass F -1 F G = F -1 F G
6 f1ococnv1 F : A 1-1 onto B F -1 F = I A
7 1 6 syl φ F -1 F = I A
8 7 coeq1d φ F -1 F G = I A G
9 fcoi2 G : B A I A G = G
10 2 9 syl φ I A G = G
11 8 10 eqtrd φ F -1 F G = G
12 5 11 eqtr3id φ F -1 F G = G
13 f1ocnv F : A 1-1 onto B F -1 : B 1-1 onto A
14 1 13 syl φ F -1 : B 1-1 onto A
15 f1of F -1 : B 1-1 onto A F -1 : B A
16 14 15 syl φ F -1 : B A
17 fcoi1 F -1 : B A F -1 I B = F -1
18 16 17 syl φ F -1 I B = F -1
19 4 12 18 3eqtr3rd φ F -1 = G