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