This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fnfco

Description: Composition of two functions. (Contributed by NM, 22-May-2006)

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

Step	Hyp	Ref	Expression
1		df-f	$⊢ G : B ⟶ A \leftrightarrow (G Fn B \land ran G \subseteq A)$
2		fnco	$⊢ (F Fn A \land G Fn B \land ran G \subseteq A) \to (F \circ G) Fn B$
3	2	3expb	$⊢ (F Fn A \land (G Fn B \land ran G \subseteq A)) \to (F \circ G) Fn B$
4	1 3	sylan2b	$⊢ (F Fn A \land G : B ⟶ A) \to (F \circ G) Fn B$