Metamath Proof Explorer


Theorem curry2val

Description: The value of a curried function with a constant second argument. (Contributed by NM, 16-Dec-2008)

Ref Expression
Hypothesis curry2.1
|- G = ( F o. `' ( 1st |` ( _V X. { C } ) ) )
Assertion curry2val
|- ( ( F Fn ( A X. B ) /\ C e. B ) -> ( G ` D ) = ( D F C ) )

Proof

Step Hyp Ref Expression
1 curry2.1
 |-  G = ( F o. `' ( 1st |` ( _V X. { C } ) ) )
2 1 curry2
 |-  ( ( F Fn ( A X. B ) /\ C e. B ) -> G = ( x e. A |-> ( x F C ) ) )
3 2 fveq1d
 |-  ( ( F Fn ( A X. B ) /\ C e. B ) -> ( G ` D ) = ( ( x e. A |-> ( x F C ) ) ` D ) )
4 eqid
 |-  ( x e. A |-> ( x F C ) ) = ( x e. A |-> ( x F C ) )
5 4 fvmptndm
 |-  ( -. D e. A -> ( ( x e. A |-> ( x F C ) ) ` D ) = (/) )
6 5 adantl
 |-  ( ( F Fn ( A X. B ) /\ -. D e. A ) -> ( ( x e. A |-> ( x F C ) ) ` D ) = (/) )
7 fndm
 |-  ( F Fn ( A X. B ) -> dom F = ( A X. B ) )
8 simpl
 |-  ( ( D e. A /\ C e. B ) -> D e. A )
9 8 con3i
 |-  ( -. D e. A -> -. ( D e. A /\ C e. B ) )
10 ndmovg
 |-  ( ( dom F = ( A X. B ) /\ -. ( D e. A /\ C e. B ) ) -> ( D F C ) = (/) )
11 7 9 10 syl2an
 |-  ( ( F Fn ( A X. B ) /\ -. D e. A ) -> ( D F C ) = (/) )
12 6 11 eqtr4d
 |-  ( ( F Fn ( A X. B ) /\ -. D e. A ) -> ( ( x e. A |-> ( x F C ) ) ` D ) = ( D F C ) )
13 12 ex
 |-  ( F Fn ( A X. B ) -> ( -. D e. A -> ( ( x e. A |-> ( x F C ) ) ` D ) = ( D F C ) ) )
14 13 adantr
 |-  ( ( F Fn ( A X. B ) /\ C e. B ) -> ( -. D e. A -> ( ( x e. A |-> ( x F C ) ) ` D ) = ( D F C ) ) )
15 oveq1
 |-  ( x = D -> ( x F C ) = ( D F C ) )
16 ovex
 |-  ( D F C ) e. _V
17 15 4 16 fvmpt
 |-  ( D e. A -> ( ( x e. A |-> ( x F C ) ) ` D ) = ( D F C ) )
18 14 17 pm2.61d2
 |-  ( ( F Fn ( A X. B ) /\ C e. B ) -> ( ( x e. A |-> ( x F C ) ) ` D ) = ( D F C ) )
19 3 18 eqtrd
 |-  ( ( F Fn ( A X. B ) /\ C e. B ) -> ( G ` D ) = ( D F C ) )