# 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 ${⊢}{\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}↾}_{{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}↾}_{{B}}$
4 3 coeq2d ${⊢}{\phi }\to {{F}}^{-1}\circ \left({F}\circ {G}\right)={{F}}^{-1}\circ \left({\mathrm{I}↾}_{{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}↾}_{{A}}$
7 1 6 syl ${⊢}{\phi }\to {{F}}^{-1}\circ {F}={\mathrm{I}↾}_{{A}}$
8 7 coeq1d ${⊢}{\phi }\to \left({{F}}^{-1}\circ {F}\right)\circ {G}=\left({\mathrm{I}↾}_{{A}}\right)\circ {G}$
9 fcoi2 ${⊢}{G}:{B}⟶{A}\to \left({\mathrm{I}↾}_{{A}}\right)\circ {G}={G}$
10 2 9 syl ${⊢}{\phi }\to \left({\mathrm{I}↾}_{{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}↾}_{{B}}\right)={{F}}^{-1}$
18 16 17 syl ${⊢}{\phi }\to {{F}}^{-1}\circ \left({\mathrm{I}↾}_{{B}}\right)={{F}}^{-1}$
19 4 12 18 3eqtr3rd ${⊢}{\phi }\to {{F}}^{-1}={G}$