Theorem funresfunco

Description: Composition of two functions, generalization of funco . (Contributed by Alexander van der Vekens, 25-Jul-2017)

	Ref	Expression
Assertion	funresfunco	$$⊢\left(\mathrm{Fun}\left({F\upharpoonright }_{\mathrm{ran}G}\right)\wedge \mathrm{Fun}G\right)\to \mathrm{Fun}\left(F\circ G\right)$$

Proof

Step	Hyp	Ref	Expression
1		funco	$$⊢\left(\mathrm{Fun}\left({F\upharpoonright }_{\mathrm{ran}G}\right)\wedge \mathrm{Fun}G\right)\to \mathrm{Fun}\left(\left({F\upharpoonright }_{\mathrm{ran}G}\right)\circ G\right)$$
2		ssid	$$⊢\mathrm{ran}G\subseteq \mathrm{ran}G$$
3		cores	$$⊢\mathrm{ran}G\subseteq \mathrm{ran}G\to \left({F\upharpoonright }_{\mathrm{ran}G}\right)\circ G=F\circ G$$
4	2 3	ax-mp	$$⊢\left({F\upharpoonright }_{\mathrm{ran}G}\right)\circ G=F\circ G$$
5	4	eqcomi	$$⊢F\circ G=\left({F\upharpoonright }_{\mathrm{ran}G}\right)\circ G$$
6	5	funeqi	$$⊢\mathrm{Fun}\left(F\circ G\right)\leftrightarrow \mathrm{Fun}\left(\left({F\upharpoonright }_{\mathrm{ran}G}\right)\circ G\right)$$
7	1 6	sylibr	$$⊢\left(\mathrm{Fun}\left({F\upharpoonright }_{\mathrm{ran}G}\right)\wedge \mathrm{Fun}G\right)\to \mathrm{Fun}\left(F\circ G\right)$$