Step |
Hyp |
Ref |
Expression |
1 |
|
curry2ima.1 |
|- G = ( F o. `' ( 1st |` ( _V X. { C } ) ) ) |
2 |
|
simp1 |
|- ( ( F Fn ( A X. B ) /\ C e. B /\ D C_ A ) -> F Fn ( A X. B ) ) |
3 |
|
dffn2 |
|- ( F Fn ( A X. B ) <-> F : ( A X. B ) --> _V ) |
4 |
2 3
|
sylib |
|- ( ( F Fn ( A X. B ) /\ C e. B /\ D C_ A ) -> F : ( A X. B ) --> _V ) |
5 |
|
simp2 |
|- ( ( F Fn ( A X. B ) /\ C e. B /\ D C_ A ) -> C e. B ) |
6 |
1
|
curry2f |
|- ( ( F : ( A X. B ) --> _V /\ C e. B ) -> G : A --> _V ) |
7 |
4 5 6
|
syl2anc |
|- ( ( F Fn ( A X. B ) /\ C e. B /\ D C_ A ) -> G : A --> _V ) |
8 |
7
|
ffund |
|- ( ( F Fn ( A X. B ) /\ C e. B /\ D C_ A ) -> Fun G ) |
9 |
|
simp3 |
|- ( ( F Fn ( A X. B ) /\ C e. B /\ D C_ A ) -> D C_ A ) |
10 |
7
|
fdmd |
|- ( ( F Fn ( A X. B ) /\ C e. B /\ D C_ A ) -> dom G = A ) |
11 |
9 10
|
sseqtrrd |
|- ( ( F Fn ( A X. B ) /\ C e. B /\ D C_ A ) -> D C_ dom G ) |
12 |
|
dfimafn |
|- ( ( Fun G /\ D C_ dom G ) -> ( G " D ) = { y | E. x e. D ( G ` x ) = y } ) |
13 |
8 11 12
|
syl2anc |
|- ( ( F Fn ( A X. B ) /\ C e. B /\ D C_ A ) -> ( G " D ) = { y | E. x e. D ( G ` x ) = y } ) |
14 |
1
|
curry2val |
|- ( ( F Fn ( A X. B ) /\ C e. B ) -> ( G ` x ) = ( x F C ) ) |
15 |
14
|
3adant3 |
|- ( ( F Fn ( A X. B ) /\ C e. B /\ D C_ A ) -> ( G ` x ) = ( x F C ) ) |
16 |
15
|
eqeq1d |
|- ( ( F Fn ( A X. B ) /\ C e. B /\ D C_ A ) -> ( ( G ` x ) = y <-> ( x F C ) = y ) ) |
17 |
|
eqcom |
|- ( ( x F C ) = y <-> y = ( x F C ) ) |
18 |
16 17
|
bitrdi |
|- ( ( F Fn ( A X. B ) /\ C e. B /\ D C_ A ) -> ( ( G ` x ) = y <-> y = ( x F C ) ) ) |
19 |
18
|
rexbidv |
|- ( ( F Fn ( A X. B ) /\ C e. B /\ D C_ A ) -> ( E. x e. D ( G ` x ) = y <-> E. x e. D y = ( x F C ) ) ) |
20 |
19
|
abbidv |
|- ( ( F Fn ( A X. B ) /\ C e. B /\ D C_ A ) -> { y | E. x e. D ( G ` x ) = y } = { y | E. x e. D y = ( x F C ) } ) |
21 |
13 20
|
eqtrd |
|- ( ( F Fn ( A X. B ) /\ C e. B /\ D C_ A ) -> ( G " D ) = { y | E. x e. D y = ( x F C ) } ) |