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 )