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 )