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

Metamath Proof Explorer

Theorem fcomptss

Description: Express composition of two functions as a maps-to applying both in sequence. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses fcomptss.a ⊢ φ → F : A ⟶ B
fcomptss.b ⊢ φ → B ⊆ C
fcomptss.g ⊢ φ → G : C ⟶ D
Assertion fcomptss ⊢ φ → G ∘ F = x ∈ A ⟼ G ⁡ F ⁡ x

Proof

Step Hyp Ref Expression
1 fcomptss.a ⊢ φ → F : A ⟶ B
2 fcomptss.b ⊢ φ → B ⊆ C
3 fcomptss.g ⊢ φ → G : C ⟶ D
4 1 2 fssd ⊢ φ → F : A ⟶ C
5 fcompt ⊢ G : C ⟶ D ∧ F : A ⟶ C → G ∘ F = x ∈ A ⟼ G ⁡ F ⁡ x
6 3 4 5 syl2anc ⊢ φ → G ∘ F = x ∈ A ⟼ G ⁡ F ⁡ x