Step |
Hyp |
Ref |
Expression |
1 |
|
curry2.1 |
|- G = ( F o. `' ( 1st |` ( _V X. { C } ) ) ) |
2 |
|
ffn |
|- ( F : ( A X. B ) --> D -> F Fn ( A X. B ) ) |
3 |
1
|
curry2 |
|- ( ( F Fn ( A X. B ) /\ C e. B ) -> G = ( x e. A |-> ( x F C ) ) ) |
4 |
2 3
|
sylan |
|- ( ( F : ( A X. B ) --> D /\ C e. B ) -> G = ( x e. A |-> ( x F C ) ) ) |
5 |
|
fovrn |
|- ( ( F : ( A X. B ) --> D /\ x e. A /\ C e. B ) -> ( x F C ) e. D ) |
6 |
5
|
3com23 |
|- ( ( F : ( A X. B ) --> D /\ C e. B /\ x e. A ) -> ( x F C ) e. D ) |
7 |
6
|
3expa |
|- ( ( ( F : ( A X. B ) --> D /\ C e. B ) /\ x e. A ) -> ( x F C ) e. D ) |
8 |
4 7
|
fmpt3d |
|- ( ( F : ( A X. B ) --> D /\ C e. B ) -> G : A --> D ) |