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

Metamath Proof Explorer

Theorem curry1val

Description: The value of a curried function with a constant first argument. (Contributed by NM, 28-Mar-2008) (Revised by Mario Carneiro, 26-Apr-2015)

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

Proof

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