Step |
Hyp |
Ref |
Expression |
1 |
|
xmetdcn2.1 |
⊢ 𝐽 = ( MetOpen ‘ 𝐷 ) |
2 |
|
metdcn.2 |
⊢ 𝐾 = ( TopOpen ‘ ℂfld ) |
3 |
2
|
tgioo2 |
⊢ ( topGen ‘ ran (,) ) = ( 𝐾 ↾t ℝ ) |
4 |
3
|
oveq2i |
⊢ ( ( 𝐽 ×t 𝐽 ) Cn ( topGen ‘ ran (,) ) ) = ( ( 𝐽 ×t 𝐽 ) Cn ( 𝐾 ↾t ℝ ) ) |
5 |
2
|
cnfldtop |
⊢ 𝐾 ∈ Top |
6 |
|
cnrest2r |
⊢ ( 𝐾 ∈ Top → ( ( 𝐽 ×t 𝐽 ) Cn ( 𝐾 ↾t ℝ ) ) ⊆ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) ) |
7 |
5 6
|
ax-mp |
⊢ ( ( 𝐽 ×t 𝐽 ) Cn ( 𝐾 ↾t ℝ ) ) ⊆ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) |
8 |
4 7
|
eqsstri |
⊢ ( ( 𝐽 ×t 𝐽 ) Cn ( topGen ‘ ran (,) ) ) ⊆ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) |
9 |
|
eqid |
⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) ) |
10 |
1 9
|
metdcn2 |
⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ( 𝐽 ×t 𝐽 ) Cn ( topGen ‘ ran (,) ) ) ) |
11 |
8 10
|
sselid |
⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) ) |