Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld ) |
2 |
1
|
dfii3 |
⊢ II = ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,] 1 ) ) |
3 |
1
|
cnfldtopon |
⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) |
4 |
3
|
a1i |
⊢ ( ⊤ → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ) |
5 |
|
unitsscn |
⊢ ( 0 [,] 1 ) ⊆ ℂ |
6 |
5
|
a1i |
⊢ ( ⊤ → ( 0 [,] 1 ) ⊆ ℂ ) |
7 |
1
|
mpomulcn |
⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) |
8 |
7
|
a1i |
⊢ ( ⊤ → ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) ) |
9 |
2 4 6 2 4 6 8
|
cnmpt2res |
⊢ ( ⊤ → ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( II ×t II ) Cn ( TopOpen ‘ ℂfld ) ) ) |
10 |
9
|
mptru |
⊢ ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( II ×t II ) Cn ( TopOpen ‘ ℂfld ) ) |
11 |
|
iimulcl |
⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) → ( 𝑥 · 𝑦 ) ∈ ( 0 [,] 1 ) ) |
12 |
11
|
rgen2 |
⊢ ∀ 𝑥 ∈ ( 0 [,] 1 ) ∀ 𝑦 ∈ ( 0 [,] 1 ) ( 𝑥 · 𝑦 ) ∈ ( 0 [,] 1 ) |
13 |
|
eqid |
⊢ ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) |
14 |
13
|
fmpo |
⊢ ( ∀ 𝑥 ∈ ( 0 [,] 1 ) ∀ 𝑦 ∈ ( 0 [,] 1 ) ( 𝑥 · 𝑦 ) ∈ ( 0 [,] 1 ) ↔ ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ ( 0 [,] 1 ) ) |
15 |
|
frn |
⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ ( 0 [,] 1 ) → ran ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ⊆ ( 0 [,] 1 ) ) |
16 |
14 15
|
sylbi |
⊢ ( ∀ 𝑥 ∈ ( 0 [,] 1 ) ∀ 𝑦 ∈ ( 0 [,] 1 ) ( 𝑥 · 𝑦 ) ∈ ( 0 [,] 1 ) → ran ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ⊆ ( 0 [,] 1 ) ) |
17 |
12 16
|
ax-mp |
⊢ ran ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ⊆ ( 0 [,] 1 ) |
18 |
|
cnrest2 |
⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ran ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ⊆ ( 0 [,] 1 ) ∧ ( 0 [,] 1 ) ⊆ ℂ ) → ( ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( II ×t II ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( II ×t II ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,] 1 ) ) ) ) ) |
19 |
3 17 5 18
|
mp3an |
⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( II ×t II ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( II ×t II ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,] 1 ) ) ) ) |
20 |
10 19
|
mpbi |
⊢ ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( II ×t II ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,] 1 ) ) ) |
21 |
2
|
oveq2i |
⊢ ( ( II ×t II ) Cn II ) = ( ( II ×t II ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,] 1 ) ) ) |
22 |
20 21
|
eleqtrri |
⊢ ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( II ×t II ) Cn II ) |