Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Glauco Siliprandi
Functions
fcoss
Metamath Proof Explorer
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
⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) : 𝐷 ⟶ 𝐵 )