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 eqtr3id
 |-  ( 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 )