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 ⊢ φ → F : A ⟶ 1-1 onto B
fcof1oinvd.g ⊢ φ → G : B ⟶ A
fcof1oinvd.b ⊢ φ → F ∘ G = I ↾ B
Assertion fcof1oinvd ⊢ φ → F -1 = G

Proof

Step Hyp Ref Expression
1 fcof1oinvd.f ⊢ φ → F : A ⟶ 1-1 onto B
2 fcof1oinvd.g ⊢ φ → G : B ⟶ A
3 fcof1oinvd.b ⊢ φ → F ∘ G = I ↾ B
4 3 coeq2d ⊢ φ → F -1 ∘ F ∘ G = F -1 ∘ I ↾ B
5 coass ⊢ F -1 ∘ F ∘ G = F -1 ∘ F ∘ G
6 f1ococnv1 ⊢ F : A ⟶ 1-1 onto B → F -1 ∘ F = I ↾ A
7 1 6 syl ⊢ φ → F -1 ∘ F = I ↾ A
8 7 coeq1d ⊢ φ → F -1 ∘ F ∘ G = I ↾ A ∘ G
9 fcoi2 ⊢ G : B ⟶ A → I ↾ A ∘ G = G
10 2 9 syl ⊢ φ → I ↾ A ∘ G = G
11 8 10 eqtrd ⊢ φ → F -1 ∘ F ∘ G = G
12 5 11 eqtr3id ⊢ φ → F -1 ∘ F ∘ G = G
13 f1ocnv ⊢ F : A ⟶ 1-1 onto B → F -1 : B ⟶ 1-1 onto A
14 f1of ⊢ F -1 : B ⟶ 1-1 onto A → F -1 : B ⟶ A
15 fcoi1 ⊢ F -1 : B ⟶ A → F -1 ∘ I ↾ B = F -1
16 1 13 14 15 4syl ⊢ φ → F -1 ∘ I ↾ B = F -1
17 4 12 16 3eqtr3rd ⊢ φ → F -1 = G