Theorem fco2

Description: Functionality of a composition with weakened out of domain condition on the first argument. (Contributed by Stefan O'Rear, 11-Mar-2015)

	Ref	Expression
Assertion	fco2	|- ( ( ( F |` B ) : B --> C /\ G : A --> B ) -> ( F o. G ) : A --> C )

Proof

Step	Hyp	Ref	Expression
1		fco	|- ( ( ( F |` B ) : B --> C /\ G : A --> B ) -> ( ( F |` B ) o. G ) : A --> C )
2		frn	|- ( G : A --> B -> ran G C_ B )
3		cores	|- ( ran G C_ B -> ( ( F |` B ) o. G ) = ( F o. G ) )
4	2 3	syl	|- ( G : A --> B -> ( ( F |` B ) o. G ) = ( F o. G ) )
5	4	adantl	|- ( ( ( F |` B ) : B --> C /\ G : A --> B ) -> ( ( F |` B ) o. G ) = ( F o. G ) )
6	5	feq1d	|- ( ( ( F |` B ) : B --> C /\ G : A --> B ) -> ( ( ( F |` B ) o. G ) : A --> C <-> ( F o. G ) : A --> C ) )
7	1 6	mpbid	|- ( ( ( F |` B ) : B --> C /\ G : A --> B ) -> ( F o. G ) : A --> C )