Theorem 1stcof

Description: Composition of the first member function with another function. (Contributed by NM, 12-Oct-2007)

	Ref	Expression
Assertion	1stcof	$$⊢F:A⟶B\times C\to \left(1^{st}\circ F\right):A⟶B$$

Proof

Step	Hyp	Ref	Expression
1		fo1st	$$⊢1^{st}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}$$
2		fofn	$$⊢1^{st}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}\to 1^{st}Fn\mathrm{V}$$
3	1 2	ax-mp	$$⊢1^{st}Fn\mathrm{V}$$
4		ffn	$$⊢F:A⟶B\times C\to FFnA$$
5		dffn2	$$⊢FFnA\leftrightarrow F:A⟶\mathrm{V}$$
6	4 5	sylib	$$⊢F:A⟶B\times C\to F:A⟶\mathrm{V}$$
7		fnfco	$$⊢\left(1^{st}Fn\mathrm{V}\wedge F:A⟶\mathrm{V}\right)\to \left(1^{st}\circ F\right)FnA$$
8	3 6 7	sylancr	$$⊢F:A⟶B\times C\to \left(1^{st}\circ F\right)FnA$$
9		rnco	$$⊢\mathrm{ran}\left(1^{st}\circ F\right)=\mathrm{ran}\left({1^{st}\upharpoonright }_{\mathrm{ran}F}\right)$$
10		frn	$$⊢F:A⟶B\times C\to \mathrm{ran}F\subseteq B\times C$$
11		ssres2	$$⊢\mathrm{ran}F\subseteq B\times C\to {1^{st}\upharpoonright }_{\mathrm{ran}F}\subseteq {1^{st}\upharpoonright }_{\left(B\times C\right)}$$
12		rnss	$$⊢{1^{st}\upharpoonright }_{\mathrm{ran}F}\subseteq {1^{st}\upharpoonright }_{\left(B\times C\right)}\to \mathrm{ran}\left({1^{st}\upharpoonright }_{\mathrm{ran}F}\right)\subseteq \mathrm{ran}\left({1^{st}\upharpoonright }_{\left(B\times C\right)}\right)$$
13	10 11 12	3syl	$$⊢F:A⟶B\times C\to \mathrm{ran}\left({1^{st}\upharpoonright }_{\mathrm{ran}F}\right)\subseteq \mathrm{ran}\left({1^{st}\upharpoonright }_{\left(B\times C\right)}\right)$$
14		f1stres	$$⊢\left({1^{st}\upharpoonright }_{\left(B\times C\right)}\right):B\times C⟶B$$
15		frn	$$⊢\left({1^{st}\upharpoonright }_{\left(B\times C\right)}\right):B\times C⟶B\to \mathrm{ran}\left({1^{st}\upharpoonright }_{\left(B\times C\right)}\right)\subseteq B$$
16	14 15	ax-mp	$$⊢\mathrm{ran}\left({1^{st}\upharpoonright }_{\left(B\times C\right)}\right)\subseteq B$$
17	13 16	sstrdi	$$⊢F:A⟶B\times C\to \mathrm{ran}\left({1^{st}\upharpoonright }_{\mathrm{ran}F}\right)\subseteq B$$
18	9 17	eqsstrid	$$⊢F:A⟶B\times C\to \mathrm{ran}\left(1^{st}\circ F\right)\subseteq B$$
19		df-f	$$⊢\left(1^{st}\circ F\right):A⟶B\leftrightarrow \left(\left(1^{st}\circ F\right)FnA\wedge \mathrm{ran}\left(1^{st}\circ F\right)\subseteq B\right)$$
20	8 18 19	sylanbrc	$$⊢F:A⟶B\times C\to \left(1^{st}\circ F\right):A⟶B$$