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 ) )