Theorem fco3

Description: Functionality of a composition. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	fco3.1	$$⊢\phi \to \mathrm{Fun}F$$
	fco3.2	$$⊢\phi \to \mathrm{Fun}G$$
Assertion	fco3	$$⊢\phi \to \left(F\circ G\right):G^{-1}\left[\mathrm{dom}F\right]⟶\mathrm{ran}F$$

Proof

Step	Hyp	Ref	Expression
1		fco3.1	$$⊢\phi \to \mathrm{Fun}F$$
2		fco3.2	$$⊢\phi \to \mathrm{Fun}G$$
3		funco	$$⊢\left(\mathrm{Fun}F\wedge \mathrm{Fun}G\right)\to \mathrm{Fun}\left(F\circ G\right)$$
4	1 2 3	syl2anc	$$⊢\phi \to \mathrm{Fun}\left(F\circ G\right)$$
5		fdmrn	$$⊢\mathrm{Fun}\left(F\circ G\right)\leftrightarrow \left(F\circ G\right):\mathrm{dom}\left(F\circ G\right)⟶\mathrm{ran}\left(F\circ G\right)$$
6	4 5	sylib	$$⊢\phi \to \left(F\circ G\right):\mathrm{dom}\left(F\circ G\right)⟶\mathrm{ran}\left(F\circ G\right)$$
7		dmco	$$⊢\mathrm{dom}\left(F\circ G\right)=G^{-1}\left[\mathrm{dom}F\right]$$
8	7	feq2i	$$⊢\left(F\circ G\right):\mathrm{dom}\left(F\circ G\right)⟶\mathrm{ran}\left(F\circ G\right)\leftrightarrow \left(F\circ G\right):G^{-1}\left[\mathrm{dom}F\right]⟶\mathrm{ran}\left(F\circ G\right)$$
9	6 8	sylib	$$⊢\phi \to \left(F\circ G\right):G^{-1}\left[\mathrm{dom}F\right]⟶\mathrm{ran}\left(F\circ G\right)$$
10		rncoss	$$⊢\mathrm{ran}\left(F\circ G\right)\subseteq \mathrm{ran}F$$
11	10	a1i	$$⊢\phi \to \mathrm{ran}\left(F\circ G\right)\subseteq \mathrm{ran}F$$
12	9 11	fssd	$$⊢\phi \to \left(F\circ G\right):G^{-1}\left[\mathrm{dom}F\right]⟶\mathrm{ran}F$$