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 (2^{nd} \circ F) : A ⟶ C$

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

Metamath Proof Explorer