This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cofmpt2

Description: Express composition of a maps-to function with another function in a maps-to notation. (Contributed by Thierry Arnoux, 15-Jul-2023)

Ref Expression
Hypotheses cofmpt2.1 
|- ( ( ph /\ y = ( F ` x ) ) -> C = D )
cofmpt2.2 
|- ( ( ph /\ y e. B ) -> C e. E )
cofmpt2.3 
|- ( ph -> F : A --> B )
cofmpt2.4 
|- ( ph -> D e. V )
Assertion cofmpt2 
|- ( ph -> ( ( y e. B |-> C ) o. F ) = ( x e. A |-> D ) )

Proof

Step Hyp Ref Expression
1 cofmpt2.1 
 |-  ( ( ph /\ y = ( F ` x ) ) -> C = D )
2 cofmpt2.2 
 |-  ( ( ph /\ y e. B ) -> C e. E )
3 cofmpt2.3 
 |-  ( ph -> F : A --> B )
4 cofmpt2.4 
 |-  ( ph -> D e. V )
5 2 fmpttd 
 |-  ( ph -> ( y e. B |-> C ) : B --> E )
6 fcompt 
 |-  ( ( ( y e. B |-> C ) : B --> E /\ F : A --> B ) -> ( ( y e. B |-> C ) o. F ) = ( x e. A |-> ( ( y e. B |-> C ) ` ( F ` x ) ) ) )
7 5 3 6 syl2anc 
 |-  ( ph -> ( ( y e. B |-> C ) o. F ) = ( x e. A |-> ( ( y e. B |-> C ) ` ( F ` x ) ) ) )
8 eqid 
 |-  ( y e. B |-> C ) = ( y e. B |-> C )
9 1 adantlr 
 |-  ( ( ( ph /\ x e. A ) /\ y = ( F ` x ) ) -> C = D )
10 3 ffvelcdmda 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) e. B )
11 4 adantr 
 |-  ( ( ph /\ x e. A ) -> D e. V )
12 8 9 10 11 fvmptd2 
 |-  ( ( ph /\ x e. A ) -> ( ( y e. B |-> C ) ` ( F ` x ) ) = D )
13 12 mpteq2dva 
 |-  ( ph -> ( x e. A |-> ( ( y e. B |-> C ) ` ( F ` x ) ) ) = ( x e. A |-> D ) )
14 7 13 eqtrd 
 |-  ( ph -> ( ( y e. B |-> C ) o. F ) = ( x e. A |-> D ) )