Theorem fnco

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

	Ref	Expression
Assertion	fnco	|- ( ( F Fn A /\ G Fn B /\ ran G C_ A ) -> ( F o. G ) Fn B )

Proof

Step	Hyp	Ref	Expression
1		fnfun	|- ( F Fn A -> Fun F )
2		fnfun	|- ( G Fn B -> Fun G )
3		funco	|- ( ( Fun F /\ Fun G ) -> Fun ( F o. G ) )
4	1 2 3	syl2an	|- ( ( F Fn A /\ G Fn B ) -> Fun ( F o. G ) )
5	4	3adant3	|- ( ( F Fn A /\ G Fn B /\ ran G C_ A ) -> Fun ( F o. G ) )
6		fndm	|- ( F Fn A -> dom F = A )
7	6	sseq2d	|- ( F Fn A -> ( ran G C_ dom F <-> ran G C_ A ) )
8	7	biimpar	|- ( ( F Fn A /\ ran G C_ A ) -> ran G C_ dom F )
9		dmcosseq	|- ( ran G C_ dom F -> dom ( F o. G ) = dom G )
10	8 9	syl	|- ( ( F Fn A /\ ran G C_ A ) -> dom ( F o. G ) = dom G )
11	10	3adant2	|- ( ( F Fn A /\ G Fn B /\ ran G C_ A ) -> dom ( F o. G ) = dom G )
12		fndm	|- ( G Fn B -> dom G = B )
13	12	3ad2ant2	|- ( ( F Fn A /\ G Fn B /\ ran G C_ A ) -> dom G = B )
14	11 13	eqtrd	|- ( ( F Fn A /\ G Fn B /\ ran G C_ A ) -> dom ( F o. G ) = B )
15		df-fn	|- ( ( F o. G ) Fn B <-> ( Fun ( F o. G ) /\ dom ( F o. G ) = B ) )
16	5 14 15	sylanbrc	|- ( ( F Fn A /\ G Fn B /\ ran G C_ A ) -> ( F o. G ) Fn B )