This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 f1of 
 |-  ( `' F : B -1-1-onto-> A -> `' F : B --> A )
15 fcoi1 
 |-  ( `' F : B --> A -> ( `' F o. ( _I |` B ) ) = `' F )
16 1 13 14 15 4syl 
 |-  ( ph -> ( `' F o. ( _I |` B ) ) = `' F )
17 4 12 16 3eqtr3rd 
 |-  ( ph -> `' F = G )