Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld ) |
2 |
|
eqid |
⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) ) |
3 |
1 2
|
abscn |
⊢ abs ∈ ( ( TopOpen ‘ ℂfld ) Cn ( topGen ‘ ran (,) ) ) |
4 |
|
ssid |
⊢ ℂ ⊆ ℂ |
5 |
|
ax-resscn |
⊢ ℝ ⊆ ℂ |
6 |
1
|
cnfldtopon |
⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) |
7 |
6
|
toponunii |
⊢ ℂ = ∪ ( TopOpen ‘ ℂfld ) |
8 |
7
|
restid |
⊢ ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld ) ) |
9 |
6 8
|
ax-mp |
⊢ ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld ) |
10 |
9
|
eqcomi |
⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) |
11 |
1
|
tgioo2 |
⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) |
12 |
1 10 11
|
cncfcn |
⊢ ( ( ℂ ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( ℂ –cn→ ℝ ) = ( ( TopOpen ‘ ℂfld ) Cn ( topGen ‘ ran (,) ) ) ) |
13 |
4 5 12
|
mp2an |
⊢ ( ℂ –cn→ ℝ ) = ( ( TopOpen ‘ ℂfld ) Cn ( topGen ‘ ran (,) ) ) |
14 |
3 13
|
eleqtrri |
⊢ abs ∈ ( ℂ –cn→ ℝ ) |