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	$$⊢\phi \to F:A⟶B$$
	fcoss.c	$$⊢\phi \to C\subseteq A$$
	fcoss.g	$$⊢\phi \to G:D⟶C$$
Assertion	fcoss	$$⊢\phi \to \left(F\circ G\right):D⟶B$$

Proof

Step	Hyp	Ref	Expression
1		fcoss.f	$$⊢\phi \to F:A⟶B$$
2		fcoss.c	$$⊢\phi \to C\subseteq A$$
3		fcoss.g	$$⊢\phi \to G:D⟶C$$
4	3 2	fssd	$$⊢\phi \to G:D⟶A$$
5		fco	$$⊢\left(F:A⟶B\wedge G:D⟶A\right)\to \left(F\circ G\right):D⟶B$$
6	1 4 5	syl2anc	$$⊢\phi \to \left(F\circ G\right):D⟶B$$