Step |
Hyp |
Ref |
Expression |
1 |
|
mulcncf.1 |
|- ( ph -> ( x e. X |-> A ) e. ( X -cn-> CC ) ) |
2 |
|
mulcncf.2 |
|- ( ph -> ( x e. X |-> B ) e. ( X -cn-> CC ) ) |
3 |
|
eqid |
|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld ) |
4 |
3
|
cnfldtopon |
|- ( TopOpen ` CCfld ) e. ( TopOn ` CC ) |
5 |
|
cncfrss |
|- ( ( x e. X |-> A ) e. ( X -cn-> CC ) -> X C_ CC ) |
6 |
1 5
|
syl |
|- ( ph -> X C_ CC ) |
7 |
|
resttopon |
|- ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ X C_ CC ) -> ( ( TopOpen ` CCfld ) |`t X ) e. ( TopOn ` X ) ) |
8 |
4 6 7
|
sylancr |
|- ( ph -> ( ( TopOpen ` CCfld ) |`t X ) e. ( TopOn ` X ) ) |
9 |
|
ssid |
|- CC C_ CC |
10 |
|
eqid |
|- ( ( TopOpen ` CCfld ) |`t X ) = ( ( TopOpen ` CCfld ) |`t X ) |
11 |
4
|
toponrestid |
|- ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC ) |
12 |
3 10 11
|
cncfcn |
|- ( ( X C_ CC /\ CC C_ CC ) -> ( X -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t X ) Cn ( TopOpen ` CCfld ) ) ) |
13 |
6 9 12
|
sylancl |
|- ( ph -> ( X -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t X ) Cn ( TopOpen ` CCfld ) ) ) |
14 |
1 13
|
eleqtrd |
|- ( ph -> ( x e. X |-> A ) e. ( ( ( TopOpen ` CCfld ) |`t X ) Cn ( TopOpen ` CCfld ) ) ) |
15 |
2 13
|
eleqtrd |
|- ( ph -> ( x e. X |-> B ) e. ( ( ( TopOpen ` CCfld ) |`t X ) Cn ( TopOpen ` CCfld ) ) ) |
16 |
4
|
a1i |
|- ( ph -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) ) |
17 |
3
|
mpomulcn |
|- ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) |
18 |
17
|
a1i |
|- ( ph -> ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) ) |
19 |
|
oveq12 |
|- ( ( u = A /\ v = B ) -> ( u x. v ) = ( A x. B ) ) |
20 |
8 14 15 16 16 18 19
|
cnmpt12 |
|- ( ph -> ( x e. X |-> ( A x. B ) ) e. ( ( ( TopOpen ` CCfld ) |`t X ) Cn ( TopOpen ` CCfld ) ) ) |
21 |
20 13
|
eleqtrrd |
|- ( ph -> ( x e. X |-> ( A x. B ) ) e. ( X -cn-> CC ) ) |