Theorem fcoss

Description: Composition of two mappings. Similar to fco , but with a weaker condition on the domain of F . (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	fcoss.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	fcoss.c	⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
	fcoss.g	⊢ ( 𝜑 → 𝐺 : 𝐷 ⟶ 𝐶 )
Assertion	fcoss	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) : 𝐷 ⟶ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fcoss.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2		fcoss.c	⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
3		fcoss.g	⊢ ( 𝜑 → 𝐺 : 𝐷 ⟶ 𝐶 )
4	3 2	fssd	⊢ ( 𝜑 → 𝐺 : 𝐷 ⟶ 𝐴 )
5		fco	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐷 ⟶ 𝐴 ) → ( 𝐹 ∘ 𝐺 ) : 𝐷 ⟶ 𝐵 )
6	1 4 5	syl2anc	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) : 𝐷 ⟶ 𝐵 )