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

Metamath Proof Explorer

Theorem mpocurryvald

Description: The value of a curried operation given in maps-to notation is a function over the second argument of the original operation. (Contributed by AV, 27-Oct-2019)

Ref Expression
Hypotheses mpocurryd.f 
|- F = ( x e. X , y e. Y |-> C )
mpocurryd.c 
|- ( ph -> A. x e. X A. y e. Y C e. V )
mpocurryd.n 
|- ( ph -> Y =/= (/) )
mpocurryvald.y 
|- ( ph -> Y e. W )
mpocurryvald.a 
|- ( ph -> A e. X )
Assertion mpocurryvald 
|- ( ph -> ( curry F ` A ) = ( y e. Y |-> [_ A / x ]_ C ) )

Proof

Step Hyp Ref Expression
1 mpocurryd.f 
 |-  F = ( x e. X , y e. Y |-> C )
2 mpocurryd.c 
 |-  ( ph -> A. x e. X A. y e. Y C e. V )
3 mpocurryd.n 
 |-  ( ph -> Y =/= (/) )
4 mpocurryvald.y 
 |-  ( ph -> Y e. W )
5 mpocurryvald.a 
 |-  ( ph -> A e. X )
6 1 2 3 mpocurryd 
 |-  ( ph -> curry F = ( x e. X |-> ( y e. Y |-> C ) ) )
7 nfcv 
 |-  F/_ a ( y e. Y |-> C )
8 nfcv 
 |-  F/_ x Y
9 nfcsb1v 
 |-  F/_ x [_ a / x ]_ C
10 8 9 nfmpt 
 |-  F/_ x ( y e. Y |-> [_ a / x ]_ C )
11 csbeq1a 
 |-  ( x = a -> C = [_ a / x ]_ C )
12 11 mpteq2dv 
 |-  ( x = a -> ( y e. Y |-> C ) = ( y e. Y |-> [_ a / x ]_ C ) )
13 7 10 12 cbvmpt 
 |-  ( x e. X |-> ( y e. Y |-> C ) ) = ( a e. X |-> ( y e. Y |-> [_ a / x ]_ C ) )
14 6 13 eqtrdi 
 |-  ( ph -> curry F = ( a e. X |-> ( y e. Y |-> [_ a / x ]_ C ) ) )
15 csbeq1 
 |-  ( a = A -> [_ a / x ]_ C = [_ A / x ]_ C )
16 15 adantl 
 |-  ( ( ph /\ a = A ) -> [_ a / x ]_ C = [_ A / x ]_ C )
17 16 mpteq2dv 
 |-  ( ( ph /\ a = A ) -> ( y e. Y |-> [_ a / x ]_ C ) = ( y e. Y |-> [_ A / x ]_ C ) )
18 4 mptexd 
 |-  ( ph -> ( y e. Y |-> [_ A / x ]_ C ) e. _V )
19 14 17 5 18 fvmptd 
 |-  ( ph -> ( curry F ` A ) = ( y e. Y |-> [_ A / x ]_ C ) )