Step |
Hyp |
Ref |
Expression |
1 |
|
resclunitintvd.1 |
|- ( ph -> ( x e. CC |-> A ) e. ( CC -cn-> CC ) ) |
2 |
|
unitsscn |
|- ( 0 [,] 1 ) C_ CC |
3 |
|
resmpt |
|- ( ( 0 [,] 1 ) C_ CC -> ( ( x e. CC |-> A ) |` ( 0 [,] 1 ) ) = ( x e. ( 0 [,] 1 ) |-> A ) ) |
4 |
2 3
|
ax-mp |
|- ( ( x e. CC |-> A ) |` ( 0 [,] 1 ) ) = ( x e. ( 0 [,] 1 ) |-> A ) |
5 |
|
rescncf |
|- ( ( 0 [,] 1 ) C_ CC -> ( ( x e. CC |-> A ) e. ( CC -cn-> CC ) -> ( ( x e. CC |-> A ) |` ( 0 [,] 1 ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) ) ) |
6 |
2 5
|
ax-mp |
|- ( ( x e. CC |-> A ) e. ( CC -cn-> CC ) -> ( ( x e. CC |-> A ) |` ( 0 [,] 1 ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) ) |
7 |
1 6
|
syl |
|- ( ph -> ( ( x e. CC |-> A ) |` ( 0 [,] 1 ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) ) |
8 |
4 7
|
eqeltrrid |
|- ( ph -> ( x e. ( 0 [,] 1 ) |-> A ) e. ( ( 0 [,] 1 ) -cn-> CC ) ) |