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 ( 𝜑𝐹 : 𝐴1-1-onto𝐵 )
fcof1oinvd.g ( 𝜑𝐺 : 𝐵𝐴 )
fcof1oinvd.b ( 𝜑 → ( 𝐹𝐺 ) = ( I ↾ 𝐵 ) )
Assertion fcof1oinvd ( 𝜑 𝐹 = 𝐺 )

Proof

Step Hyp Ref Expression
1 fcof1oinvd.f ( 𝜑𝐹 : 𝐴1-1-onto𝐵 )
2 fcof1oinvd.g ( 𝜑𝐺 : 𝐵𝐴 )
3 fcof1oinvd.b ( 𝜑 → ( 𝐹𝐺 ) = ( I ↾ 𝐵 ) )
4 3 coeq2d ( 𝜑 → ( 𝐹 ∘ ( 𝐹𝐺 ) ) = ( 𝐹 ∘ ( I ↾ 𝐵 ) ) )
5 coass ( ( 𝐹𝐹 ) ∘ 𝐺 ) = ( 𝐹 ∘ ( 𝐹𝐺 ) )
6 f1ococnv1 ( 𝐹 : 𝐴1-1-onto𝐵 → ( 𝐹𝐹 ) = ( I ↾ 𝐴 ) )
7 1 6 syl ( 𝜑 → ( 𝐹𝐹 ) = ( I ↾ 𝐴 ) )
8 7 coeq1d ( 𝜑 → ( ( 𝐹𝐹 ) ∘ 𝐺 ) = ( ( I ↾ 𝐴 ) ∘ 𝐺 ) )
9 fcoi2 ( 𝐺 : 𝐵𝐴 → ( ( I ↾ 𝐴 ) ∘ 𝐺 ) = 𝐺 )
10 2 9 syl ( 𝜑 → ( ( I ↾ 𝐴 ) ∘ 𝐺 ) = 𝐺 )
11 8 10 eqtrd ( 𝜑 → ( ( 𝐹𝐹 ) ∘ 𝐺 ) = 𝐺 )
12 5 11 eqtr3id ( 𝜑 → ( 𝐹 ∘ ( 𝐹𝐺 ) ) = 𝐺 )
13 f1ocnv ( 𝐹 : 𝐴1-1-onto𝐵 𝐹 : 𝐵1-1-onto𝐴 )
14 1 13 syl ( 𝜑 𝐹 : 𝐵1-1-onto𝐴 )
15 f1of ( 𝐹 : 𝐵1-1-onto𝐴 𝐹 : 𝐵𝐴 )
16 14 15 syl ( 𝜑 𝐹 : 𝐵𝐴 )
17 fcoi1 ( 𝐹 : 𝐵𝐴 → ( 𝐹 ∘ ( I ↾ 𝐵 ) ) = 𝐹 )
18 16 17 syl ( 𝜑 → ( 𝐹 ∘ ( I ↾ 𝐵 ) ) = 𝐹 )
19 4 12 18 3eqtr3rd ( 𝜑 𝐹 = 𝐺 )