Theorem fnresfnco

Description: Composition of two functions, similar to fnco . (Contributed by Alexander van der Vekens, 25-Jul-2017)

	Ref	Expression
Assertion	fnresfnco	|- ( ( ( F |` ran G ) Fn ran G /\ G Fn B ) -> ( F o. G ) Fn B )

Proof

Step	Hyp	Ref	Expression
1		fnfun	|- ( ( F |` ran G ) Fn ran G -> Fun ( F |` ran G ) )
2		fnfun	|- ( G Fn B -> Fun G )
3		funresfunco	|- ( ( Fun ( F |` ran G ) /\ Fun G ) -> Fun ( F o. G ) )
4	1 2 3	syl2an	|- ( ( ( F |` ran G ) Fn ran G /\ G Fn B ) -> Fun ( F o. G ) )
5		fndm	|- ( ( F |` ran G ) Fn ran G -> dom ( F |` ran G ) = ran G )
6		dmres	|- dom ( F |` ran G ) = ( ran G i^i dom F )
7	6	eqeq1i	|- ( dom ( F |` ran G ) = ran G <-> ( ran G i^i dom F ) = ran G )
8		df-ss	|- ( ran G C_ dom F <-> ( ran G i^i dom F ) = ran G )
9	7 8	sylbb2	|- ( dom ( F |` ran G ) = ran G -> ran G C_ dom F )
10	5 9	syl	|- ( ( F |` ran G ) Fn ran G -> ran G C_ dom F )
11	10	adantr	|- ( ( ( F |` ran G ) Fn ran G /\ G Fn B ) -> ran G C_ dom F )
12		dmcosseq	|- ( ran G C_ dom F -> dom ( F o. G ) = dom G )
13	11 12	syl	|- ( ( ( F |` ran G ) Fn ran G /\ G Fn B ) -> dom ( F o. G ) = dom G )
14		fndm	|- ( G Fn B -> dom G = B )
15	14	adantl	|- ( ( ( F |` ran G ) Fn ran G /\ G Fn B ) -> dom G = B )
16	13 15	eqtrd	|- ( ( ( F |` ran G ) Fn ran G /\ G Fn B ) -> dom ( F o. G ) = B )
17		df-fn	|- ( ( F o. G ) Fn B <-> ( Fun ( F o. G ) /\ dom ( F o. G ) = B ) )
18	4 16 17	sylanbrc	|- ( ( ( F |` ran G ) Fn ran G /\ G Fn B ) -> ( F o. G ) Fn B )