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 )