Step | Hyp | Ref
| Expression |
1 | | df1o2 7459 |
. . . 4
⊢
1𝑜 = {∅} |
2 | | snfi 7923 |
. . . 4
⊢ {∅}
∈ Fin |
3 | 1, 2 | eqeltri 2684 |
. . 3
⊢
1𝑜 ∈ Fin |
4 | | imassrn 5396 |
. . . . 5
⊢ ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) ⊆ ran
(𝑥 ∈ ℝ ↦
({∅} × {𝑥})) |
5 | | 0ex 4718 |
. . . . . . . . . 10
⊢ ∅
∈ V |
6 | | eqid 2610 |
. . . . . . . . . . 11
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − )
↾ (ℝ × ℝ)) |
7 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ ↦
({∅} × {𝑥})) =
(𝑥 ∈ ℝ ↦
({∅} × {𝑥})) |
8 | 6, 7 | ismrer1 32807 |
. . . . . . . . . 10
⊢ (∅
∈ V → (𝑥 ∈
ℝ ↦ ({∅} × {𝑥})) ∈ (((abs ∘ − ) ↾
(ℝ × ℝ)) Ismty
(ℝn‘{∅}))) |
9 | 5, 8 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
∈ (((abs ∘ − ) ↾ (ℝ × ℝ)) Ismty
(ℝn‘{∅})) |
10 | 1 | fveq2i 6106 |
. . . . . . . . . 10
⊢
(ℝn‘1𝑜) =
(ℝn‘{∅}) |
11 | 10 | oveq2i 6560 |
. . . . . . . . 9
⊢ (((abs
∘ − ) ↾ (ℝ × ℝ)) Ismty
(ℝn‘1𝑜)) = (((abs ∘
− ) ↾ (ℝ × ℝ)) Ismty
(ℝn‘{∅})) |
12 | 9, 11 | eleqtrri 2687 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
∈ (((abs ∘ − ) ↾ (ℝ × ℝ)) Ismty
(ℝn‘1𝑜)) |
13 | 6 | rexmet 22402 |
. . . . . . . . 9
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) |
14 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (ℝ
↑𝑚 1𝑜) = (ℝ
↑𝑚 1𝑜) |
15 | 14 | rrnmet 32798 |
. . . . . . . . . 10
⊢
(1𝑜 ∈ Fin →
(ℝn‘1𝑜) ∈
(Met‘(ℝ ↑𝑚
1𝑜))) |
16 | | metxmet 21949 |
. . . . . . . . . 10
⊢
((ℝn‘1𝑜) ∈
(Met‘(ℝ ↑𝑚 1𝑜)) →
(ℝn‘1𝑜) ∈
(∞Met‘(ℝ ↑𝑚
1𝑜))) |
17 | 3, 15, 16 | mp2b 10 |
. . . . . . . . 9
⊢
(ℝn‘1𝑜) ∈
(∞Met‘(ℝ ↑𝑚
1𝑜)) |
18 | | isismty 32770 |
. . . . . . . . 9
⊢ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) ∧
(ℝn‘1𝑜) ∈
(∞Met‘(ℝ ↑𝑚 1𝑜)))
→ ((𝑥 ∈ ℝ
↦ ({∅} × {𝑥})) ∈ (((abs ∘ − ) ↾
(ℝ × ℝ)) Ismty
(ℝn‘1𝑜)) ↔ ((𝑥 ∈ ℝ ↦
({∅} × {𝑥})):ℝ–1-1-onto→(ℝ ↑𝑚
1𝑜) ∧ ∀𝑦 ∈ ℝ ∀𝑧 ∈ ℝ (𝑦((abs ∘ − ) ↾ (ℝ
× ℝ))𝑧) =
(((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))‘𝑦)(ℝn‘1𝑜)((𝑥 ∈ ℝ ↦ ({∅} × {𝑥}))‘𝑧))))) |
19 | 13, 17, 18 | mp2an 704 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
∈ (((abs ∘ − ) ↾ (ℝ × ℝ)) Ismty
(ℝn‘1𝑜)) ↔ ((𝑥 ∈ ℝ ↦
({∅} × {𝑥})):ℝ–1-1-onto→(ℝ ↑𝑚
1𝑜) ∧ ∀𝑦 ∈ ℝ ∀𝑧 ∈ ℝ (𝑦((abs ∘ − ) ↾ (ℝ
× ℝ))𝑧) =
(((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))‘𝑦)(ℝn‘1𝑜)((𝑥 ∈ ℝ ↦ ({∅} × {𝑥}))‘𝑧)))) |
20 | 12, 19 | mpbi 219 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ↦
({∅} × {𝑥})):ℝ–1-1-onto→(ℝ ↑𝑚
1𝑜) ∧ ∀𝑦 ∈ ℝ ∀𝑧 ∈ ℝ (𝑦((abs ∘ − ) ↾ (ℝ
× ℝ))𝑧) =
(((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))‘𝑦)(ℝn‘1𝑜)((𝑥 ∈ ℝ ↦ ({∅} × {𝑥}))‘𝑧))) |
21 | 20 | simpli 473 |
. . . . . 6
⊢ (𝑥 ∈ ℝ ↦
({∅} × {𝑥})):ℝ–1-1-onto→(ℝ ↑𝑚
1𝑜) |
22 | | f1of 6050 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ↦
({∅} × {𝑥})):ℝ–1-1-onto→(ℝ ↑𝑚
1𝑜) → (𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})):ℝ⟶(ℝ
↑𝑚 1𝑜)) |
23 | | frn 5966 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ↦
({∅} × {𝑥})):ℝ⟶(ℝ
↑𝑚 1𝑜) → ran (𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
⊆ (ℝ ↑𝑚
1𝑜)) |
24 | 21, 22, 23 | mp2b 10 |
. . . . 5
⊢ ran
(𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
⊆ (ℝ ↑𝑚
1𝑜) |
25 | 4, 24 | sstri 3577 |
. . . 4
⊢ ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) ⊆ (ℝ
↑𝑚 1𝑜) |
26 | 25 | a1i 11 |
. . 3
⊢ (𝑌 ⊆ ℝ → ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) ⊆ (ℝ
↑𝑚 1𝑜)) |
27 | | eqid 2610 |
. . . 4
⊢
((ℝn‘1𝑜) ↾
(((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌))) =
((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌))) |
28 | | eqid 2610 |
. . . 4
⊢
(MetOpen‘((ℝn‘1𝑜)
↾ (((𝑥 ∈ ℝ
↦ ({∅} × {𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌)))) =
(MetOpen‘((ℝn‘1𝑜)
↾ (((𝑥 ∈ ℝ
↦ ({∅} × {𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌)))) |
29 | | eqid 2610 |
. . . 4
⊢
(MetOpen‘(ℝn‘1𝑜))
=
(MetOpen‘(ℝn‘1𝑜)) |
30 | 14, 27, 28, 29 | rrnheibor 32806 |
. . 3
⊢
((1𝑜 ∈ Fin ∧ ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) ⊆ (ℝ
↑𝑚 1𝑜)) →
((MetOpen‘((ℝn‘1𝑜)
↾ (((𝑥 ∈ ℝ
↦ ({∅} × {𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌)))) ∈ Comp ↔ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) ∈
(Clsd‘(MetOpen‘(ℝn‘1𝑜)))
∧ ((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦ ({∅}
× {𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} × {𝑥})) “ 𝑌))) ∈ (Bnd‘((𝑥 ∈ ℝ ↦ ({∅} × {𝑥})) “ 𝑌))))) |
31 | 3, 26, 30 | sylancr 694 |
. 2
⊢ (𝑌 ⊆ ℝ →
((MetOpen‘((ℝn‘1𝑜)
↾ (((𝑥 ∈ ℝ
↦ ({∅} × {𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌)))) ∈ Comp ↔ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) ∈
(Clsd‘(MetOpen‘(ℝn‘1𝑜)))
∧ ((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦ ({∅}
× {𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} × {𝑥})) “ 𝑌))) ∈ (Bnd‘((𝑥 ∈ ℝ ↦ ({∅} × {𝑥})) “ 𝑌))))) |
32 | | reheibor.2 |
. . . . . . 7
⊢ 𝑀 = ((abs ∘ − )
↾ (𝑌 × 𝑌)) |
33 | | cnxmet 22386 |
. . . . . . . 8
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
34 | | id 22 |
. . . . . . . . 9
⊢ (𝑌 ⊆ ℝ → 𝑌 ⊆
ℝ) |
35 | | ax-resscn 9872 |
. . . . . . . . 9
⊢ ℝ
⊆ ℂ |
36 | 34, 35 | syl6ss 3580 |
. . . . . . . 8
⊢ (𝑌 ⊆ ℝ → 𝑌 ⊆
ℂ) |
37 | | xmetres2 21976 |
. . . . . . . 8
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑌 ⊆ ℂ) → ((abs ∘
− ) ↾ (𝑌
× 𝑌)) ∈
(∞Met‘𝑌)) |
38 | 33, 36, 37 | sylancr 694 |
. . . . . . 7
⊢ (𝑌 ⊆ ℝ → ((abs
∘ − ) ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌)) |
39 | 32, 38 | syl5eqel 2692 |
. . . . . 6
⊢ (𝑌 ⊆ ℝ → 𝑀 ∈ (∞Met‘𝑌)) |
40 | | xmetres2 21976 |
. . . . . . 7
⊢
(((ℝn‘1𝑜) ∈
(∞Met‘(ℝ ↑𝑚 1𝑜))
∧ ((𝑥 ∈ ℝ
↦ ({∅} × {𝑥})) “ 𝑌) ⊆ (ℝ
↑𝑚 1𝑜)) →
((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌))) ∈
(∞Met‘((𝑥
∈ ℝ ↦ ({∅} × {𝑥})) “ 𝑌))) |
41 | 17, 26, 40 | sylancr 694 |
. . . . . 6
⊢ (𝑌 ⊆ ℝ →
((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌))) ∈
(∞Met‘((𝑥
∈ ℝ ↦ ({∅} × {𝑥})) “ 𝑌))) |
42 | | reheibor.3 |
. . . . . . 7
⊢ 𝑇 = (MetOpen‘𝑀) |
43 | 42, 28 | ismtyhmeo 32774 |
. . . . . 6
⊢ ((𝑀 ∈ (∞Met‘𝑌) ∧
((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌))) ∈
(∞Met‘((𝑥
∈ ℝ ↦ ({∅} × {𝑥})) “ 𝑌))) → (𝑀 Ismty
((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌)))) ⊆
(𝑇Homeo(MetOpen‘((ℝn‘1𝑜)
↾ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) × ((𝑥 ∈
ℝ ↦ ({∅} × {𝑥})) “ 𝑌)))))) |
44 | 39, 41, 43 | syl2anc 691 |
. . . . 5
⊢ (𝑌 ⊆ ℝ → (𝑀 Ismty
((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌)))) ⊆
(𝑇Homeo(MetOpen‘((ℝn‘1𝑜)
↾ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) × ((𝑥 ∈
ℝ ↦ ({∅} × {𝑥})) “ 𝑌)))))) |
45 | 13 | a1i 11 |
. . . . . . 7
⊢ (𝑌 ⊆ ℝ → ((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ)) |
46 | 17 | a1i 11 |
. . . . . . 7
⊢ (𝑌 ⊆ ℝ →
(ℝn‘1𝑜) ∈
(∞Met‘(ℝ ↑𝑚
1𝑜))) |
47 | 12 | a1i 11 |
. . . . . . 7
⊢ (𝑌 ⊆ ℝ → (𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
∈ (((abs ∘ − ) ↾ (ℝ × ℝ)) Ismty
(ℝn‘1𝑜))) |
48 | | eqid 2610 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) = ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) |
49 | | eqid 2610 |
. . . . . . . 8
⊢ (((abs
∘ − ) ↾ (ℝ × ℝ)) ↾ (𝑌 × 𝑌)) = (((abs ∘ − ) ↾
(ℝ × ℝ)) ↾ (𝑌 × 𝑌)) |
50 | 48, 49, 27 | ismtyres 32777 |
. . . . . . 7
⊢ (((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) ∧
(ℝn‘1𝑜) ∈
(∞Met‘(ℝ ↑𝑚 1𝑜)))
∧ ((𝑥 ∈ ℝ
↦ ({∅} × {𝑥})) ∈ (((abs ∘ − ) ↾
(ℝ × ℝ)) Ismty
(ℝn‘1𝑜)) ∧ 𝑌 ⊆ ℝ)) →
((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
↾ 𝑌) ∈ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ↾ (𝑌 × 𝑌)) Ismty
((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌))))) |
51 | 45, 46, 47, 34, 50 | syl22anc 1319 |
. . . . . 6
⊢ (𝑌 ⊆ ℝ → ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
↾ 𝑌) ∈ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ↾ (𝑌 × 𝑌)) Ismty
((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌))))) |
52 | | xpss12 5148 |
. . . . . . . . . 10
⊢ ((𝑌 ⊆ ℝ ∧ 𝑌 ⊆ ℝ) → (𝑌 × 𝑌) ⊆ (ℝ ×
ℝ)) |
53 | 52 | anidms 675 |
. . . . . . . . 9
⊢ (𝑌 ⊆ ℝ → (𝑌 × 𝑌) ⊆ (ℝ ×
ℝ)) |
54 | 53 | resabs1d 5348 |
. . . . . . . 8
⊢ (𝑌 ⊆ ℝ → (((abs
∘ − ) ↾ (ℝ × ℝ)) ↾ (𝑌 × 𝑌)) = ((abs ∘ − ) ↾ (𝑌 × 𝑌))) |
55 | 54, 32 | syl6eqr 2662 |
. . . . . . 7
⊢ (𝑌 ⊆ ℝ → (((abs
∘ − ) ↾ (ℝ × ℝ)) ↾ (𝑌 × 𝑌)) = 𝑀) |
56 | 55 | oveq1d 6564 |
. . . . . 6
⊢ (𝑌 ⊆ ℝ → ((((abs
∘ − ) ↾ (ℝ × ℝ)) ↾ (𝑌 × 𝑌)) Ismty
((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌)))) = (𝑀 Ismty
((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌))))) |
57 | 51, 56 | eleqtrd 2690 |
. . . . 5
⊢ (𝑌 ⊆ ℝ → ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
↾ 𝑌) ∈ (𝑀 Ismty
((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌))))) |
58 | 44, 57 | sseldd 3569 |
. . . 4
⊢ (𝑌 ⊆ ℝ → ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
↾ 𝑌) ∈ (𝑇Homeo(MetOpen‘((ℝn‘1𝑜)
↾ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) × ((𝑥 ∈
ℝ ↦ ({∅} × {𝑥})) “ 𝑌)))))) |
59 | | hmphi 21390 |
. . . 4
⊢ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
↾ 𝑌) ∈ (𝑇Homeo(MetOpen‘((ℝn‘1𝑜)
↾ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) × ((𝑥 ∈
ℝ ↦ ({∅} × {𝑥})) “ 𝑌))))) → 𝑇 ≃
(MetOpen‘((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦ ({∅} × {𝑥})) “ 𝑌) ×
((𝑥 ∈ ℝ ↦ ({∅} × {𝑥})) “ 𝑌))))) |
60 | 58, 59 | syl 17 |
. . 3
⊢ (𝑌 ⊆ ℝ → 𝑇 ≃
(MetOpen‘((ℝn‘1𝑜)
↾ (((𝑥 ∈ ℝ
↦ ({∅} × {𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌))))) |
61 | | cmphmph 21401 |
. . . 4
⊢ (𝑇 ≃
(MetOpen‘((ℝn‘1𝑜)
↾ (((𝑥 ∈ ℝ
↦ ({∅} × {𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌)))) → (𝑇 ∈ Comp →
(MetOpen‘((ℝn‘1𝑜)
↾ (((𝑥 ∈ ℝ
↦ ({∅} × {𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌)))) ∈
Comp)) |
62 | | hmphsym 21395 |
. . . . 5
⊢ (𝑇 ≃
(MetOpen‘((ℝn‘1𝑜)
↾ (((𝑥 ∈ ℝ
↦ ({∅} × {𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌)))) →
(MetOpen‘((ℝn‘1𝑜)
↾ (((𝑥 ∈ ℝ
↦ ({∅} × {𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌)))) ≃ 𝑇) |
63 | | cmphmph 21401 |
. . . . 5
⊢
((MetOpen‘((ℝn‘1𝑜)
↾ (((𝑥 ∈ ℝ
↦ ({∅} × {𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌)))) ≃ 𝑇 →
((MetOpen‘((ℝn‘1𝑜)
↾ (((𝑥 ∈ ℝ
↦ ({∅} × {𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌)))) ∈ Comp → 𝑇 ∈ Comp)) |
64 | 62, 63 | syl 17 |
. . . 4
⊢ (𝑇 ≃
(MetOpen‘((ℝn‘1𝑜)
↾ (((𝑥 ∈ ℝ
↦ ({∅} × {𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌)))) →
((MetOpen‘((ℝn‘1𝑜)
↾ (((𝑥 ∈ ℝ
↦ ({∅} × {𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌)))) ∈ Comp → 𝑇 ∈ Comp)) |
65 | 61, 64 | impbid 201 |
. . 3
⊢ (𝑇 ≃
(MetOpen‘((ℝn‘1𝑜)
↾ (((𝑥 ∈ ℝ
↦ ({∅} × {𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌)))) → (𝑇 ∈ Comp ↔
(MetOpen‘((ℝn‘1𝑜)
↾ (((𝑥 ∈ ℝ
↦ ({∅} × {𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌)))) ∈
Comp)) |
66 | 60, 65 | syl 17 |
. 2
⊢ (𝑌 ⊆ ℝ → (𝑇 ∈ Comp ↔
(MetOpen‘((ℝn‘1𝑜)
↾ (((𝑥 ∈ ℝ
↦ ({∅} × {𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌)))) ∈
Comp)) |
67 | | reheibor.4 |
. . . . . . . 8
⊢ 𝑈 = (topGen‘ran
(,)) |
68 | | eqid 2610 |
. . . . . . . . 9
⊢
(MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) |
69 | 6, 68 | tgioo 22407 |
. . . . . . . 8
⊢
(topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾
(ℝ × ℝ))) |
70 | 67, 69 | eqtri 2632 |
. . . . . . 7
⊢ 𝑈 = (MetOpen‘((abs ∘
− ) ↾ (ℝ × ℝ))) |
71 | 70, 29 | ismtyhmeo 32774 |
. . . . . 6
⊢ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) ∧
(ℝn‘1𝑜) ∈
(∞Met‘(ℝ ↑𝑚 1𝑜)))
→ (((abs ∘ − ) ↾ (ℝ × ℝ)) Ismty
(ℝn‘1𝑜)) ⊆ (𝑈Homeo(MetOpen‘(ℝn‘1𝑜)))) |
72 | 13, 17, 71 | mp2an 704 |
. . . . 5
⊢ (((abs
∘ − ) ↾ (ℝ × ℝ)) Ismty
(ℝn‘1𝑜)) ⊆ (𝑈Homeo(MetOpen‘(ℝn‘1𝑜))) |
73 | 72, 12 | sselii 3565 |
. . . 4
⊢ (𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
∈ (𝑈Homeo(MetOpen‘(ℝn‘1𝑜))) |
74 | | retopon 22377 |
. . . . . . 7
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
75 | 67, 74 | eqeltri 2684 |
. . . . . 6
⊢ 𝑈 ∈
(TopOn‘ℝ) |
76 | 75 | toponunii 20547 |
. . . . 5
⊢ ℝ =
∪ 𝑈 |
77 | 76 | hmeocld 21380 |
. . . 4
⊢ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
∈ (𝑈Homeo(MetOpen‘(ℝn‘1𝑜)))
∧ 𝑌 ⊆ ℝ) → (𝑌 ∈ (Clsd‘𝑈)
↔ ((𝑥 ∈ ℝ ↦ ({∅} × {𝑥})) “ 𝑌)
∈ (Clsd‘(MetOpen‘(ℝn‘1𝑜))))) |
78 | 73, 34, 77 | sylancr 694 |
. . 3
⊢ (𝑌 ⊆ ℝ → (𝑌 ∈ (Clsd‘𝑈) ↔ ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) ∈
(Clsd‘(MetOpen‘(ℝn‘1𝑜))))) |
79 | | ismtybnd 32776 |
. . . 4
⊢ ((𝑀 ∈ (∞Met‘𝑌) ∧
((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌))) ∈
(∞Met‘((𝑥
∈ ℝ ↦ ({∅} × {𝑥})) “ 𝑌)) ∧ ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) ↾ 𝑌) ∈ (𝑀 Ismty
((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌))))) →
(𝑀 ∈ (Bnd‘𝑌) ↔
((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌))) ∈
(Bnd‘((𝑥 ∈
ℝ ↦ ({∅} × {𝑥})) “ 𝑌)))) |
80 | 39, 41, 57, 79 | syl3anc 1318 |
. . 3
⊢ (𝑌 ⊆ ℝ → (𝑀 ∈ (Bnd‘𝑌) ↔
((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌))) ∈
(Bnd‘((𝑥 ∈
ℝ ↦ ({∅} × {𝑥})) “ 𝑌)))) |
81 | 78, 80 | anbi12d 743 |
. 2
⊢ (𝑌 ⊆ ℝ → ((𝑌 ∈ (Clsd‘𝑈) ∧ 𝑀 ∈ (Bnd‘𝑌)) ↔ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) ∈
(Clsd‘(MetOpen‘(ℝn‘1𝑜)))
∧ ((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦ ({∅}
× {𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} × {𝑥})) “ 𝑌))) ∈ (Bnd‘((𝑥 ∈ ℝ ↦ ({∅} × {𝑥})) “ 𝑌))))) |
82 | 31, 66, 81 | 3bitr4d 299 |
1
⊢ (𝑌 ⊆ ℝ → (𝑇 ∈ Comp ↔ (𝑌 ∈ (Clsd‘𝑈) ∧ 𝑀 ∈ (Bnd‘𝑌)))) |