Step |
Hyp |
Ref |
Expression |
1 |
|
iihalf2cn.1 |
⊢ 𝐽 = ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) |
2 |
|
eqid |
⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld ) |
3 |
|
dfii2 |
⊢ II = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) ) |
4 |
|
halfre |
⊢ ( 1 / 2 ) ∈ ℝ |
5 |
|
1re |
⊢ 1 ∈ ℝ |
6 |
|
iccssre |
⊢ ( ( ( 1 / 2 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 1 / 2 ) [,] 1 ) ⊆ ℝ ) |
7 |
4 5 6
|
mp2an |
⊢ ( ( 1 / 2 ) [,] 1 ) ⊆ ℝ |
8 |
7
|
a1i |
⊢ ( ⊤ → ( ( 1 / 2 ) [,] 1 ) ⊆ ℝ ) |
9 |
|
unitssre |
⊢ ( 0 [,] 1 ) ⊆ ℝ |
10 |
9
|
a1i |
⊢ ( ⊤ → ( 0 [,] 1 ) ⊆ ℝ ) |
11 |
|
iihalf2 |
⊢ ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) → ( ( 2 · 𝑥 ) − 1 ) ∈ ( 0 [,] 1 ) ) |
12 |
11
|
adantl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) ) → ( ( 2 · 𝑥 ) − 1 ) ∈ ( 0 [,] 1 ) ) |
13 |
2
|
cnfldtopon |
⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) |
14 |
13
|
a1i |
⊢ ( ⊤ → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ) |
15 |
|
2cnd |
⊢ ( ⊤ → 2 ∈ ℂ ) |
16 |
14 14 15
|
cnmptc |
⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ 2 ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) ) |
17 |
14
|
cnmptid |
⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ 𝑥 ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) ) |
18 |
2
|
mulcn |
⊢ · ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) |
19 |
18
|
a1i |
⊢ ( ⊤ → · ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) ) |
20 |
14 16 17 19
|
cnmpt12f |
⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( 2 · 𝑥 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) ) |
21 |
|
1cnd |
⊢ ( ⊤ → 1 ∈ ℂ ) |
22 |
14 14 21
|
cnmptc |
⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ 1 ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) ) |
23 |
2
|
subcn |
⊢ − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) |
24 |
23
|
a1i |
⊢ ( ⊤ → − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) ) |
25 |
14 20 22 24
|
cnmpt12f |
⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( ( 2 · 𝑥 ) − 1 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) ) |
26 |
2 1 3 8 10 12 25
|
cnmptre |
⊢ ( ⊤ → ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) ↦ ( ( 2 · 𝑥 ) − 1 ) ) ∈ ( 𝐽 Cn II ) ) |
27 |
26
|
mptru |
⊢ ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) ↦ ( ( 2 · 𝑥 ) − 1 ) ) ∈ ( 𝐽 Cn II ) |