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 )