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	|- ( ph -> F : A --> B )
	fcoss.c	|- ( ph -> C C_ A )
	fcoss.g	|- ( ph -> G : D --> C )
Assertion	fcoss	|- ( ph -> ( F o. G ) : D --> B )

Proof

Step	Hyp	Ref	Expression
1		fcoss.f	|- ( ph -> F : A --> B )
2		fcoss.c	|- ( ph -> C C_ A )
3		fcoss.g	|- ( ph -> G : D --> C )
4	3 2	fssd	|- ( ph -> G : D --> A )
5		fco	|- ( ( F : A --> B /\ G : D --> A ) -> ( F o. G ) : D --> B )
6	1 4 5	syl2anc	|- ( ph -> ( F o. G ) : D --> B )