Metamath Proof Explorer


Theorem fvcod

Description: Value of a function composition. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses fvcod.g
|- ( ph -> Fun G )
fvcod.a
|- ( ph -> A e. dom G )
fvcod.h
|- H = ( F o. G )
Assertion fvcod
|- ( ph -> ( H ` A ) = ( F ` ( G ` A ) ) )

Proof

Step Hyp Ref Expression
1 fvcod.g
 |-  ( ph -> Fun G )
2 fvcod.a
 |-  ( ph -> A e. dom G )
3 fvcod.h
 |-  H = ( F o. G )
4 3 fveq1i
 |-  ( H ` A ) = ( ( F o. G ) ` A )
5 4 a1i
 |-  ( ph -> ( H ` A ) = ( ( F o. G ) ` A ) )
6 fvco
 |-  ( ( Fun G /\ A e. dom G ) -> ( ( F o. G ) ` A ) = ( F ` ( G ` A ) ) )
7 1 2 6 syl2anc
 |-  ( ph -> ( ( F o. G ) ` A ) = ( F ` ( G ` A ) ) )
8 5 7 eqtrd
 |-  ( ph -> ( H ` A ) = ( F ` ( G ` A ) ) )