fco

Description: Composition of two mappings. (Contributed by NM, 29-Aug-1999) (Proof shortened by Andrew Salmon, 17-Sep-2011)

		Ref	Expression
	Assertion	fco	$⊢ (F : B ⟶ C \land G : A ⟶ B) \to (F \circ G) : A ⟶ C$

Step	Hyp	Ref	Expression
1		df-f	$⊢ F : B ⟶ C \leftrightarrow (F Fn B \land ran F \subseteq C)$
2		df-f	$⊢ G : A ⟶ B \leftrightarrow (G Fn A \land ran G \subseteq B)$
3		fnco	$⊢ (F Fn B \land G Fn A \land ran G \subseteq B) \to (F \circ G) Fn A$
4	3	3expib	$⊢ F Fn B \to ((G Fn A \land ran G \subseteq B) \to (F \circ G) Fn A)$
5	4	adantr	$⊢ (F Fn B \land ran F \subseteq C) \to ((G Fn A \land ran G \subseteq B) \to (F \circ G) Fn A)$
6		rncoss	$⊢ ran (F \circ G) \subseteq ran F$
7		sstr	$⊢ (ran (F \circ G) \subseteq ran F \land ran F \subseteq C) \to ran (F \circ G) \subseteq C$
8	6 7	mpan	$⊢ ran F \subseteq C \to ran (F \circ G) \subseteq C$
9	8	adantl	$⊢ (F Fn B \land ran F \subseteq C) \to ran (F \circ G) \subseteq C$
10	5 9	jctird	$⊢ (F Fn B \land ran F \subseteq C) \to ((G Fn A \land ran G \subseteq B) \to ((F \circ G) Fn A \land ran (F \circ G) \subseteq C))$
11	10	imp	$⊢ ((F Fn B \land ran F \subseteq C) \land (G Fn A \land ran G \subseteq B)) \to ((F \circ G) Fn A \land ran (F \circ G) \subseteq C)$
12	1 2 11	syl2anb	$⊢ (F : B ⟶ C \land G : A ⟶ B) \to ((F \circ G) Fn A \land ran (F \circ G) \subseteq C)$
13		df-f	$⊢ (F \circ G) : A ⟶ C \leftrightarrow ((F \circ G) Fn A \land ran (F \circ G) \subseteq C)$
14	12 13	sylibr	$⊢ (F : B ⟶ C \land G : A ⟶ B) \to (F \circ G) : A ⟶ C$

Metamath Proof Explorer