Theorem fco2

Description: Functionality of a composition with weakened out of domain condition on the first argument. (Contributed by Stefan O'Rear, 11-Mar-2015)

	Ref	Expression
Assertion	fco2	$$⊢\left(\left({F\upharpoonright }_B\right):B⟶C\wedge G:A⟶B\right)\to \left(F\circ G\right):A⟶C$$

Proof

Step	Hyp	Ref	Expression
1		fco	$$⊢\left(\left({F\upharpoonright }_B\right):B⟶C\wedge G:A⟶B\right)\to \left(\left({F\upharpoonright }_B\right)\circ G\right):A⟶C$$
2		frn	$$⊢G:A⟶B\to \mathrm{ran}G\subseteq B$$
3		cores	$$⊢\mathrm{ran}G\subseteq B\to \left({F\upharpoonright }_B\right)\circ G=F\circ G$$
4	2 3	syl	$$⊢G:A⟶B\to \left({F\upharpoonright }_B\right)\circ G=F\circ G$$
5	4	adantl	$$⊢\left(\left({F\upharpoonright }_B\right):B⟶C\wedge G:A⟶B\right)\to \left({F\upharpoonright }_B\right)\circ G=F\circ G$$
6	5	feq1d	$$⊢\left(\left({F\upharpoonright }_B\right):B⟶C\wedge G:A⟶B\right)\to \left(\left(\left({F\upharpoonright }_B\right)\circ G\right):A⟶C\leftrightarrow \left(F\circ G\right):A⟶C\right)$$
7	1 6	mpbid	$$⊢\left(\left({F\upharpoonright }_B\right):B⟶C\wedge G:A⟶B\right)\to \left(F\circ G\right):A⟶C$$