Step |
Hyp |
Ref |
Expression |
1 |
|
iihalf1cn.1 |
⊢ 𝐽 = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) |
2 |
|
eqid |
⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld ) |
3 |
|
dfii2 |
⊢ II = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) ) |
4 |
|
0red |
⊢ ( ⊤ → 0 ∈ ℝ ) |
5 |
|
halfre |
⊢ ( 1 / 2 ) ∈ ℝ |
6 |
|
iccssre |
⊢ ( ( 0 ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → ( 0 [,] ( 1 / 2 ) ) ⊆ ℝ ) |
7 |
4 5 6
|
sylancl |
⊢ ( ⊤ → ( 0 [,] ( 1 / 2 ) ) ⊆ ℝ ) |
8 |
|
unitssre |
⊢ ( 0 [,] 1 ) ⊆ ℝ |
9 |
8
|
a1i |
⊢ ( ⊤ → ( 0 [,] 1 ) ⊆ ℝ ) |
10 |
|
iihalf1 |
⊢ ( 𝑥 ∈ ( 0 [,] ( 1 / 2 ) ) → ( 2 · 𝑥 ) ∈ ( 0 [,] 1 ) ) |
11 |
10
|
adantl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 0 [,] ( 1 / 2 ) ) ) → ( 2 · 𝑥 ) ∈ ( 0 [,] 1 ) ) |
12 |
2
|
cnfldtopon |
⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) |
13 |
12
|
a1i |
⊢ ( ⊤ → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ) |
14 |
|
2cnd |
⊢ ( ⊤ → 2 ∈ ℂ ) |
15 |
13 13 14
|
cnmptc |
⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ 2 ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) ) |
16 |
13
|
cnmptid |
⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ 𝑥 ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) ) |
17 |
2
|
mpomulcn |
⊢ ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) |
18 |
17
|
a1i |
⊢ ( ⊤ → ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) ) |
19 |
|
oveq12 |
⊢ ( ( 𝑢 = 2 ∧ 𝑣 = 𝑥 ) → ( 𝑢 · 𝑣 ) = ( 2 · 𝑥 ) ) |
20 |
13 15 16 13 13 18 19
|
cnmpt12 |
⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( 2 · 𝑥 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) ) |
21 |
2 1 3 7 9 11 20
|
cnmptre |
⊢ ( ⊤ → ( 𝑥 ∈ ( 0 [,] ( 1 / 2 ) ) ↦ ( 2 · 𝑥 ) ) ∈ ( 𝐽 Cn II ) ) |
22 |
21
|
mptru |
⊢ ( 𝑥 ∈ ( 0 [,] ( 1 / 2 ) ) ↦ ( 2 · 𝑥 ) ) ∈ ( 𝐽 Cn II ) |