This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

Proof

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