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