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

Metamath Proof Explorer

Theorem f1cof1

Description: Composition of two one-to-one functions. Generalization of f1co . (Contributed by AV, 18-Sep-2024)

Ref Expression
Assertion f1cof1 
|- ( ( F : C -1-1-> D /\ G : A -1-1-> B ) -> ( F o. G ) : ( `' G " C ) -1-1-> D )

Proof

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