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 ⊢ ( 𝜑 → 𝐹 : 𝐴 –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 f1of ⊢ ( ◡ 𝐹 : 𝐵 –1-1-onto→ 𝐴 → ◡ 𝐹 : 𝐵 ⟶ 𝐴 )
15 fcoi1 ⊢ ( ◡ 𝐹 : 𝐵 ⟶ 𝐴 → ( ◡ 𝐹 ∘ ( I ↾ 𝐵 ) ) = ◡ 𝐹 )
16 1 13 14 15 4syl ⊢ ( 𝜑 → ( ◡ 𝐹 ∘ ( I ↾ 𝐵 ) ) = ◡ 𝐹 )
17 4 12 16 3eqtr3rd ⊢ ( 𝜑 → ◡ 𝐹 = 𝐺 )