Step |
Hyp |
Ref |
Expression |
1 |
|
cncfmpt2f.1 |
|- J = ( TopOpen ` CCfld ) |
2 |
|
cncfmpt2f.2 |
|- ( ph -> F e. ( ( J tX J ) Cn J ) ) |
3 |
|
cncfmpt2f.3 |
|- ( ph -> ( x e. X |-> A ) e. ( X -cn-> CC ) ) |
4 |
|
cncfmpt2f.4 |
|- ( ph -> ( x e. X |-> B ) e. ( X -cn-> CC ) ) |
5 |
1
|
cnfldtopon |
|- J e. ( TopOn ` CC ) |
6 |
|
cncfrss |
|- ( ( x e. X |-> A ) e. ( X -cn-> CC ) -> X C_ CC ) |
7 |
3 6
|
syl |
|- ( ph -> X C_ CC ) |
8 |
|
resttopon |
|- ( ( J e. ( TopOn ` CC ) /\ X C_ CC ) -> ( J |`t X ) e. ( TopOn ` X ) ) |
9 |
5 7 8
|
sylancr |
|- ( ph -> ( J |`t X ) e. ( TopOn ` X ) ) |
10 |
|
ssid |
|- CC C_ CC |
11 |
|
eqid |
|- ( J |`t X ) = ( J |`t X ) |
12 |
5
|
toponrestid |
|- J = ( J |`t CC ) |
13 |
1 11 12
|
cncfcn |
|- ( ( X C_ CC /\ CC C_ CC ) -> ( X -cn-> CC ) = ( ( J |`t X ) Cn J ) ) |
14 |
7 10 13
|
sylancl |
|- ( ph -> ( X -cn-> CC ) = ( ( J |`t X ) Cn J ) ) |
15 |
3 14
|
eleqtrd |
|- ( ph -> ( x e. X |-> A ) e. ( ( J |`t X ) Cn J ) ) |
16 |
4 14
|
eleqtrd |
|- ( ph -> ( x e. X |-> B ) e. ( ( J |`t X ) Cn J ) ) |
17 |
9 15 16 2
|
cnmpt12f |
|- ( ph -> ( x e. X |-> ( A F B ) ) e. ( ( J |`t X ) Cn J ) ) |
18 |
17 14
|
eleqtrrd |
|- ( ph -> ( x e. X |-> ( A F B ) ) e. ( X -cn-> CC ) ) |