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 (1^{st} \circ F) : A ⟶ B$

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

Metamath Proof Explorer