Theorem fcomptss

Description: Express composition of two functions as a maps-to applying both in sequence. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	fcomptss.a	|- ( ph -> F : A --> B )
	fcomptss.b	|- ( ph -> B C_ C )
	fcomptss.g	|- ( ph -> G : C --> D )
Assertion	fcomptss	|- ( ph -> ( G o. F ) = ( x e. A |-> ( G ` ( F ` x ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fcomptss.a	|- ( ph -> F : A --> B )
2		fcomptss.b	|- ( ph -> B C_ C )
3		fcomptss.g	|- ( ph -> G : C --> D )
4	1 2	fssd	|- ( ph -> F : A --> C )
5		fcompt	|- ( ( G : C --> D /\ F : A --> C ) -> ( G o. F ) = ( x e. A |-> ( G ` ( F ` x ) ) ) )
6	3 4 5	syl2anc	|- ( ph -> ( G o. F ) = ( x e. A |-> ( G ` ( F ` x ) ) ) )