Theorem fco3OLD

Description: Obsolete version of funcofd as 20-Sep-2024. (Contributed by Glauco Siliprandi, 26-Jun-2021) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		fco3OLD.1	$$⊢\phi \to \mathrm{Fun}F$$
2		fco3OLD.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$$