Metamath Proof Explorer

Theorem afv2co2

Description: Value of a function composition, analogous to fvco2 . (Contributed by AV, 8-Sep-2022)

Ref Expression
Assertion afv2co2 
|- ( ( G defAt X /\ F defAt ( G '''' X ) ) -> ( ( F o. G ) '''' X ) = ( F '''' ( G '''' X ) ) )

Proof

Step Hyp Ref Expression
1 imaco 
 |-  ( ( F o. G ) " { X } ) = ( F " ( G " { X } ) )
2 dfatsnafv2 
 |-  ( G defAt X -> { ( G '''' X ) } = ( G " { X } ) )
3 2 adantr 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> { ( G '''' X ) } = ( G " { X } ) )
4 3 imaeq2d 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> ( F " { ( G '''' X ) } ) = ( F " ( G " { X } ) ) )
5 1 4 eqtr4id 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> ( ( F o. G ) " { X } ) = ( F " { ( G '''' X ) } ) )
6 5 eleq2d 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> ( x e. ( ( F o. G ) " { X } ) <-> x e. ( F " { ( G '''' X ) } ) ) )
7 6 iotabidv 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> ( iota x x e. ( ( F o. G ) " { X } ) ) = ( iota x x e. ( F " { ( G '''' X ) } ) ) )
8 dfatco 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> ( F o. G ) defAt X )
9 dfafv23 
 |-  ( ( F o. G ) defAt X -> ( ( F o. G ) '''' X ) = ( iota x x e. ( ( F o. G ) " { X } ) ) )
10 8 9 syl 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> ( ( F o. G ) '''' X ) = ( iota x x e. ( ( F o. G ) " { X } ) ) )
11 dfafv23 
 |-  ( F defAt ( G '''' X ) -> ( F '''' ( G '''' X ) ) = ( iota x x e. ( F " { ( G '''' X ) } ) ) )
12 11 adantl 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> ( F '''' ( G '''' X ) ) = ( iota x x e. ( F " { ( G '''' X ) } ) ) )
13 7 10 12 3eqtr4d 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> ( ( F o. G ) '''' X ) = ( F '''' ( G '''' X ) ) )