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

Metamath Proof Explorer

Theorem 2fvcoidd

Description: Show that the composition of two functions is the identity function by applying both functions to each value of the domain of the first function. (Contributed by AV, 15-Dec-2019)

Ref Expression
Hypotheses 2fvcoidd.f ⊢ φ → F : A ⟶ B
2fvcoidd.g ⊢ φ → G : B ⟶ A
2fvcoidd.i ⊢ φ → ∀ a ∈ A G ⁡ F ⁡ a = a
Assertion 2fvcoidd ⊢ φ → G ∘ F = I ↾ A

Proof

Step Hyp Ref Expression
1 2fvcoidd.f ⊢ φ → F : A ⟶ B
2 2fvcoidd.g ⊢ φ → G : B ⟶ A
3 2fvcoidd.i ⊢ φ → ∀ a ∈ A G ⁡ F ⁡ a = a
4 fcompt ⊢ G : B ⟶ A ∧ F : A ⟶ B → G ∘ F = x ∈ A ⟼ G ⁡ F ⁡ x
5 2 1 4 syl2anc ⊢ φ → G ∘ F = x ∈ A ⟼ G ⁡ F ⁡ x
6 2fveq3 ⊢ a = x → G ⁡ F ⁡ a = G ⁡ F ⁡ x
7 id ⊢ a = x → a = x
8 6 7 eqeq12d ⊢ a = x → G ⁡ F ⁡ a = a ↔ G ⁡ F ⁡ x = x
9 8 rspccv ⊢ ∀ a ∈ A G ⁡ F ⁡ a = a → x ∈ A → G ⁡ F ⁡ x = x
10 3 9 syl ⊢ φ → x ∈ A → G ⁡ F ⁡ x = x
11 10 imp ⊢ φ ∧ x ∈ A → G ⁡ F ⁡ x = x
12 11 mpteq2dva ⊢ φ → x ∈ A ⟼ G ⁡ F ⁡ x = x ∈ A ⟼ x
13 mptresid ⊢ I ↾ A = x ∈ A ⟼ x
14 12 13 eqtr4di ⊢ φ → x ∈ A ⟼ G ⁡ F ⁡ x = I ↾ A
15 5 14 eqtrd ⊢ φ → G ∘ F = I ↾ A