Theorem fnfco

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

	Ref	Expression
Assertion	fnfco	$$⊢\left(FFnA\wedge G:B⟶A\right)\to \left(F\circ G\right)FnB$$

Proof

Step	Hyp	Ref	Expression
1		df-f	$$⊢G:B⟶A\leftrightarrow \left(GFnB\wedge \mathrm{ran}G\subseteq A\right)$$
2		fnco	$$⊢\left(FFnA\wedge GFnB\wedge \mathrm{ran}G\subseteq A\right)\to \left(F\circ G\right)FnB$$
3	2	3expb	$$⊢\left(FFnA\wedge \left(GFnB\wedge \mathrm{ran}G\subseteq A\right)\right)\to \left(F\circ G\right)FnB$$
4	1 3	sylan2b	$$⊢\left(FFnA\wedge G:B⟶A\right)\to \left(F\circ G\right)FnB$$