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