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

Metamath Proof Explorer

Theorem fco

Description: Composition of two functions with domain and codomain as a function with domain and codomain. (Contributed by NM, 29-Aug-1999) (Proof shortened by Andrew Salmon, 17-Sep-2011) (Proof shortened by AV, 20-Sep-2024)

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

Proof

Step Hyp Ref Expression
1 ffun 
 |-  ( G : A --> B -> Fun G )
2 fcof 
 |-  ( ( F : B --> C /\ Fun G ) -> ( F o. G ) : ( `' G " B ) --> C )
3 1 2 sylan2 
 |-  ( ( F : B --> C /\ G : A --> B ) -> ( F o. G ) : ( `' G " B ) --> C )
4 fimacnv 
 |-  ( G : A --> B -> ( `' G " B ) = A )
5 4 eqcomd 
 |-  ( G : A --> B -> A = ( `' G " B ) )
6 5 adantl 
 |-  ( ( F : B --> C /\ G : A --> B ) -> A = ( `' G " B ) )
7 6 feq2d 
 |-  ( ( F : B --> C /\ G : A --> B ) -> ( ( F o. G ) : A --> C <-> ( F o. G ) : ( `' G " B ) --> C ) )
8 3 7 mpbird 
 |-  ( ( F : B --> C /\ G : A --> B ) -> ( F o. G ) : A --> C )