Metamath Proof Explorer

Theorem f1coOLD

Description: Obsolete version of f1co as of 20-Sep-2024. (Contributed by NM, 28-May-1998) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 df-f1 
 |-  ( F : B -1-1-> C <-> ( F : B --> C /\ Fun `' F ) )
2 df-f1 
 |-  ( G : A -1-1-> B <-> ( G : A --> B /\ Fun `' G ) )
3 fco 
 |-  ( ( F : B --> C /\ G : A --> B ) -> ( F o. G ) : A --> C )
4 funco 
 |-  ( ( Fun `' G /\ Fun `' F ) -> Fun ( `' G o. `' F ) )
5 cnvco 
 |-  `' ( F o. G ) = ( `' G o. `' F )
6 5 funeqi 
 |-  ( Fun `' ( F o. G ) <-> Fun ( `' G o. `' F ) )
7 4 6 sylibr 
 |-  ( ( Fun `' G /\ Fun `' F ) -> Fun `' ( F o. G ) )
8 7 ancoms 
 |-  ( ( Fun `' F /\ Fun `' G ) -> Fun `' ( F o. G ) )
9 3 8 anim12i 
 |-  ( ( ( F : B --> C /\ G : A --> B ) /\ ( Fun `' F /\ Fun `' G ) ) -> ( ( F o. G ) : A --> C /\ Fun `' ( F o. G ) ) )
10 9 an4s 
 |-  ( ( ( F : B --> C /\ Fun `' F ) /\ ( G : A --> B /\ Fun `' G ) ) -> ( ( F o. G ) : A --> C /\ Fun `' ( F o. G ) ) )
11 1 2 10 syl2anb 
 |-  ( ( F : B -1-1-> C /\ G : A -1-1-> B ) -> ( ( F o. G ) : A --> C /\ Fun `' ( F o. G ) ) )
12 df-f1 
 |-  ( ( F o. G ) : A -1-1-> C <-> ( ( F o. G ) : A --> C /\ Fun `' ( F o. G ) ) )
13 11 12 sylibr 
 |-  ( ( F : B -1-1-> C /\ G : A -1-1-> B ) -> ( F o. G ) : A -1-1-> C )