Theorem fcod

Description: Composition of two mappings. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	fcod.1	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐶 )
	fcod.2	⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝐵 )
Assertion	fcod	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		fcod.1	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐶 )
2		fcod.2	⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝐵 )
3		fco	⊢ ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 )
4	1 2 3	syl2anc	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 )