Theorem funresfunco

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

	Ref	Expression
Assertion	funresfunco	|- ( ( Fun ( F |` ran G ) /\ Fun G ) -> Fun ( F o. G ) )

Proof

Step	Hyp	Ref	Expression
1		funco	|- ( ( Fun ( F |` ran G ) /\ Fun G ) -> Fun ( ( F |` ran G ) o. G ) )
2		ssid	|- ran G C_ ran G
3		cores	|- ( ran G C_ ran G -> ( ( F |` ran G ) o. G ) = ( F o. G ) )
4	2 3	ax-mp	|- ( ( F |` ran G ) o. G ) = ( F o. G )
5	4	eqcomi	|- ( F o. G ) = ( ( F |` ran G ) o. G )
6	5	funeqi	|- ( Fun ( F o. G ) <-> Fun ( ( F |` ran G ) o. G ) )
7	1 6	sylibr	|- ( ( Fun ( F |` ran G ) /\ Fun G ) -> Fun ( F o. G ) )