This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )