Theorem 2ndcof

Description: Composition of the second member function with another function. (Contributed by FL, 15-Oct-2012)

	Ref	Expression
Assertion	2ndcof	$$⊢F:A⟶B\times C\to \left(2^{nd}\circ F\right):A⟶C$$

Proof

Step	Hyp	Ref	Expression
1		fo2nd	$$⊢2^{nd}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}$$
2		fofn	$$⊢2^{nd}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}\to 2^{nd}Fn\mathrm{V}$$
3	1 2	ax-mp	$$⊢2^{nd}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(2^{nd}Fn\mathrm{V}\wedge F:A⟶\mathrm{V}\right)\to \left(2^{nd}\circ F\right)FnA$$
8	3 6 7	sylancr	$$⊢F:A⟶B\times C\to \left(2^{nd}\circ F\right)FnA$$
9		rnco	$$⊢\mathrm{ran}\left(2^{nd}\circ F\right)=\mathrm{ran}\left({2^{nd}\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 {2^{nd}\upharpoonright }_{\mathrm{ran}F}\subseteq {2^{nd}\upharpoonright }_{\left(B\times C\right)}$$
12		rnss	$$⊢{2^{nd}\upharpoonright }_{\mathrm{ran}F}\subseteq {2^{nd}\upharpoonright }_{\left(B\times C\right)}\to \mathrm{ran}\left({2^{nd}\upharpoonright }_{\mathrm{ran}F}\right)\subseteq \mathrm{ran}\left({2^{nd}\upharpoonright }_{\left(B\times C\right)}\right)$$
13	10 11 12	3syl	$$⊢F:A⟶B\times C\to \mathrm{ran}\left({2^{nd}\upharpoonright }_{\mathrm{ran}F}\right)\subseteq \mathrm{ran}\left({2^{nd}\upharpoonright }_{\left(B\times C\right)}\right)$$
14		f2ndres	$$⊢\left({2^{nd}\upharpoonright }_{\left(B\times C\right)}\right):B\times C⟶C$$
15		frn	$$⊢\left({2^{nd}\upharpoonright }_{\left(B\times C\right)}\right):B\times C⟶C\to \mathrm{ran}\left({2^{nd}\upharpoonright }_{\left(B\times C\right)}\right)\subseteq C$$
16	14 15	ax-mp	$$⊢\mathrm{ran}\left({2^{nd}\upharpoonright }_{\left(B\times C\right)}\right)\subseteq C$$
17	13 16	sstrdi	$$⊢F:A⟶B\times C\to \mathrm{ran}\left({2^{nd}\upharpoonright }_{\mathrm{ran}F}\right)\subseteq C$$
18	9 17	eqsstrid	$$⊢F:A⟶B\times C\to \mathrm{ran}\left(2^{nd}\circ F\right)\subseteq C$$
19		df-f	$$⊢\left(2^{nd}\circ F\right):A⟶C\leftrightarrow \left(\left(2^{nd}\circ F\right)FnA\wedge \mathrm{ran}\left(2^{nd}\circ F\right)\subseteq C\right)$$
20	8 18 19	sylanbrc	$$⊢F:A⟶B\times C\to \left(2^{nd}\circ F\right):A⟶C$$