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

Metamath Proof Explorer

Theorem f1co

Description: Composition of one-to-one functions when the codomain of the first matches the domain of the second. Exercise 30 of TakeutiZaring p. 25. (Contributed by NM, 28-May-1998) (Proof shortened by AV, 20-Sep-2024)

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

Proof

Step Hyp Ref Expression
1 f1cof1 
 |-  ( ( F : B -1-1-> C /\ G : A -1-1-> B ) -> ( F o. G ) : ( `' G " B ) -1-1-> C )
2 f1f 
 |-  ( G : A -1-1-> B -> G : A --> B )
3 fimacnv 
 |-  ( G : A --> B -> ( `' G " B ) = A )
4 2 3 syl 
 |-  ( G : A -1-1-> B -> ( `' G " B ) = A )
5 4 adantl 
 |-  ( ( F : B -1-1-> C /\ G : A -1-1-> B ) -> ( `' G " B ) = A )
6 5 eqcomd 
 |-  ( ( F : B -1-1-> C /\ G : A -1-1-> B ) -> A = ( `' G " B ) )
7 f1eq2 
 |-  ( A = ( `' G " B ) -> ( ( F o. G ) : A -1-1-> C <-> ( F o. G ) : ( `' G " B ) -1-1-> C ) )
8 6 7 syl 
 |-  ( ( F : B -1-1-> C /\ G : A -1-1-> B ) -> ( ( F o. G ) : A -1-1-> C <-> ( F o. G ) : ( `' G " B ) -1-1-> C ) )
9 1 8 mpbird 
 |-  ( ( F : B -1-1-> C /\ G : A -1-1-> B ) -> ( F o. G ) : A -1-1-> C )