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 ( 𝜑𝐹 : 𝐴𝐵 )
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 ( 𝜑 → ( 𝐹𝐺 ) : 𝐷𝐵 )