# 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
`|- ( ph -> F : A -1-1-onto-> B )`
fcof1oinvd.g
`|- ( ph -> G : B --> A )`
fcof1oinvd.b
`|- ( ph -> ( F o. G ) = ( _I |` B ) )`
Assertion fcof1oinvd
`|- ( ph -> `' F = G )`

### Proof

Step Hyp Ref Expression
1 fcof1oinvd.f
` |-  ( ph -> F : A -1-1-onto-> B )`
2 fcof1oinvd.g
` |-  ( ph -> G : B --> A )`
3 fcof1oinvd.b
` |-  ( ph -> ( F o. G ) = ( _I |` B ) )`
4 3 coeq2d
` |-  ( ph -> ( `' F o. ( F o. G ) ) = ( `' F o. ( _I |` B ) ) )`
5 coass
` |-  ( ( `' F o. F ) o. G ) = ( `' F o. ( F o. G ) )`
6 f1ococnv1
` |-  ( F : A -1-1-onto-> B -> ( `' F o. F ) = ( _I |` A ) )`
7 1 6 syl
` |-  ( ph -> ( `' F o. F ) = ( _I |` A ) )`
8 7 coeq1d
` |-  ( ph -> ( ( `' F o. F ) o. G ) = ( ( _I |` A ) o. G ) )`
9 fcoi2
` |-  ( G : B --> A -> ( ( _I |` A ) o. G ) = G )`
10 2 9 syl
` |-  ( ph -> ( ( _I |` A ) o. G ) = G )`
11 8 10 eqtrd
` |-  ( ph -> ( ( `' F o. F ) o. G ) = G )`
12 5 11 syl5eqr
` |-  ( ph -> ( `' F o. ( F o. G ) ) = G )`
13 f1ocnv
` |-  ( F : A -1-1-onto-> B -> `' F : B -1-1-onto-> A )`
14 1 13 syl
` |-  ( ph -> `' F : B -1-1-onto-> A )`
15 f1of
` |-  ( `' F : B -1-1-onto-> A -> `' F : B --> A )`
16 14 15 syl
` |-  ( ph -> `' F : B --> A )`
17 fcoi1
` |-  ( `' F : B --> A -> ( `' F o. ( _I |` B ) ) = `' F )`
18 16 17 syl
` |-  ( ph -> ( `' F o. ( _I |` B ) ) = `' F )`
19 4 12 18 3eqtr3rd
` |-  ( ph -> `' F = G )`