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 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
fcomptss.b ⊢ ( 𝜑 → 𝐵 ⊆ 𝐶 )
fcomptss.g ⊢ ( 𝜑 → 𝐺 : 𝐶 ⟶ 𝐷 )
Assertion fcomptss ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 fcomptss.a ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2 fcomptss.b ⊢ ( 𝜑 → 𝐵 ⊆ 𝐶 )
3 fcomptss.g ⊢ ( 𝜑 → 𝐺 : 𝐶 ⟶ 𝐷 )
4 1 2 fssd ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐶 )
5 fcompt ⊢ ( ( 𝐺 : 𝐶 ⟶ 𝐷 ∧ 𝐹 : 𝐴 ⟶ 𝐶 ) → ( 𝐺 ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
6 3 4 5 syl2anc ⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) )