Metamath Proof Explorer


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 ) ) ) )