Step | Hyp | Ref
| Expression |
1 | | df1o2 7970 |
. . . 4
⊢
1o = {∅} |
2 | | snfi 8445 |
. . . 4
⊢ {∅}
∈ Fin |
3 | 1, 2 | eqeltri 2878 |
. . 3
⊢
1o ∈ Fin |
4 | | imassrn 5820 |
. . . . 5
⊢ ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) ⊆ ran
(𝑥 ∈ ℝ ↦
({∅} × {𝑥})) |
5 | | 0ex 5105 |
. . . . . . . . . 10
⊢ ∅
∈ V |
6 | | eqid 2794 |
. . . . . . . . . . 11
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − )
↾ (ℝ × ℝ)) |
7 | | eqid 2794 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ ↦
({∅} × {𝑥})) =
(𝑥 ∈ ℝ ↦
({∅} × {𝑥})) |
8 | 6, 7 | ismrer1 34661 |
. . . . . . . . . 10
⊢ (∅
∈ V → (𝑥 ∈
ℝ ↦ ({∅} × {𝑥})) ∈ (((abs ∘ − ) ↾
(ℝ × ℝ)) Ismty
(ℝn‘{∅}))) |
9 | 5, 8 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
∈ (((abs ∘ − ) ↾ (ℝ × ℝ)) Ismty
(ℝn‘{∅})) |
10 | 1 | fveq2i 6544 |
. . . . . . . . . 10
⊢
(ℝn‘1o) =
(ℝn‘{∅}) |
11 | 10 | oveq2i 7030 |
. . . . . . . . 9
⊢ (((abs
∘ − ) ↾ (ℝ × ℝ)) Ismty
(ℝn‘1o)) = (((abs ∘ − )
↾ (ℝ × ℝ)) Ismty
(ℝn‘{∅})) |
12 | 9, 11 | eleqtrri 2881 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
∈ (((abs ∘ − ) ↾ (ℝ × ℝ)) Ismty
(ℝn‘1o)) |
13 | 6 | rexmet 23082 |
. . . . . . . . 9
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) |
14 | | eqid 2794 |
. . . . . . . . . . 11
⊢ (ℝ
↑𝑚 1o) = (ℝ ↑𝑚
1o) |
15 | 14 | rrnmet 34652 |
. . . . . . . . . 10
⊢
(1o ∈ Fin →
(ℝn‘1o) ∈ (Met‘(ℝ
↑𝑚 1o))) |
16 | | metxmet 22627 |
. . . . . . . . . 10
⊢
((ℝn‘1o) ∈
(Met‘(ℝ ↑𝑚 1o)) →
(ℝn‘1o) ∈
(∞Met‘(ℝ ↑𝑚
1o))) |
17 | 3, 15, 16 | mp2b 10 |
. . . . . . . . 9
⊢
(ℝn‘1o) ∈
(∞Met‘(ℝ ↑𝑚
1o)) |
18 | | isismty 34624 |
. . . . . . . . 9
⊢ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) ∧
(ℝn‘1o) ∈
(∞Met‘(ℝ ↑𝑚 1o))) →
((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
∈ (((abs ∘ − ) ↾ (ℝ × ℝ)) Ismty
(ℝn‘1o)) ↔ ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})):ℝ–1-1-onto→(ℝ ↑𝑚
1o) ∧ ∀𝑦 ∈ ℝ ∀𝑧 ∈ ℝ (𝑦((abs ∘ − ) ↾ (ℝ
× ℝ))𝑧) =
(((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))‘𝑦)(ℝn‘1o)((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥}))‘𝑧))))) |
19 | 13, 17, 18 | mp2an 688 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
∈ (((abs ∘ − ) ↾ (ℝ × ℝ)) Ismty
(ℝn‘1o)) ↔ ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})):ℝ–1-1-onto→(ℝ ↑𝑚
1o) ∧ ∀𝑦 ∈ ℝ ∀𝑧 ∈ ℝ (𝑦((abs ∘ − ) ↾ (ℝ
× ℝ))𝑧) =
(((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))‘𝑦)(ℝn‘1o)((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥}))‘𝑧)))) |
20 | 12, 19 | mpbi 231 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ↦
({∅} × {𝑥})):ℝ–1-1-onto→(ℝ ↑𝑚
1o) ∧ ∀𝑦 ∈ ℝ ∀𝑧 ∈ ℝ (𝑦((abs ∘ − ) ↾ (ℝ
× ℝ))𝑧) =
(((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))‘𝑦)(ℝn‘1o)((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥}))‘𝑧))) |
21 | 20 | simpli 484 |
. . . . . 6
⊢ (𝑥 ∈ ℝ ↦
({∅} × {𝑥})):ℝ–1-1-onto→(ℝ ↑𝑚
1o) |
22 | | f1of 6486 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ↦
({∅} × {𝑥})):ℝ–1-1-onto→(ℝ ↑𝑚
1o) → (𝑥
∈ ℝ ↦ ({∅} × {𝑥})):ℝ⟶(ℝ
↑𝑚 1o)) |
23 | | frn 6391 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ↦
({∅} × {𝑥})):ℝ⟶(ℝ
↑𝑚 1o) → ran (𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) ⊆ (ℝ
↑𝑚 1o)) |
24 | 21, 22, 23 | mp2b 10 |
. . . . 5
⊢ ran
(𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
⊆ (ℝ ↑𝑚 1o) |
25 | 4, 24 | sstri 3900 |
. . . 4
⊢ ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) ⊆ (ℝ
↑𝑚 1o) |
26 | 25 | a1i 11 |
. . 3
⊢ (𝑌 ⊆ ℝ → ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) ⊆ (ℝ
↑𝑚 1o)) |
27 | | eqid 2794 |
. . . 4
⊢
((ℝn‘1o) ↾ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌))) =
((ℝn‘1o) ↾ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌))) |
28 | | eqid 2794 |
. . . 4
⊢
(MetOpen‘((ℝn‘1o) ↾
(((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌)))) =
(MetOpen‘((ℝn‘1o) ↾
(((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌)))) |
29 | | eqid 2794 |
. . . 4
⊢
(MetOpen‘(ℝn‘1o)) =
(MetOpen‘(ℝn‘1o)) |
30 | 14, 27, 28, 29 | rrnheibor 34660 |
. . 3
⊢
((1o ∈ Fin ∧ ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) ⊆ (ℝ
↑𝑚 1o)) →
((MetOpen‘((ℝn‘1o) ↾
(((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌)))) ∈ Comp
↔ (((𝑥 ∈ ℝ
↦ ({∅} × {𝑥})) “ 𝑌) ∈
(Clsd‘(MetOpen‘(ℝn‘1o)))
∧ ((ℝn‘1o) ↾ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌))) ∈
(Bnd‘((𝑥 ∈
ℝ ↦ ({∅} × {𝑥})) “ 𝑌))))) |
31 | 3, 26, 30 | sylancr 587 |
. 2
⊢ (𝑌 ⊆ ℝ →
((MetOpen‘((ℝn‘1o) ↾
(((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌)))) ∈ Comp
↔ (((𝑥 ∈ ℝ
↦ ({∅} × {𝑥})) “ 𝑌) ∈
(Clsd‘(MetOpen‘(ℝn‘1o)))
∧ ((ℝn‘1o) ↾ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌))) ∈
(Bnd‘((𝑥 ∈
ℝ ↦ ({∅} × {𝑥})) “ 𝑌))))) |
32 | | reheibor.2 |
. . . . . . 7
⊢ 𝑀 = ((abs ∘ − )
↾ (𝑌 × 𝑌)) |
33 | | cnxmet 23064 |
. . . . . . . 8
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
34 | | id 22 |
. . . . . . . . 9
⊢ (𝑌 ⊆ ℝ → 𝑌 ⊆
ℝ) |
35 | | ax-resscn 10443 |
. . . . . . . . 9
⊢ ℝ
⊆ ℂ |
36 | 34, 35 | syl6ss 3903 |
. . . . . . . 8
⊢ (𝑌 ⊆ ℝ → 𝑌 ⊆
ℂ) |
37 | | xmetres2 22654 |
. . . . . . . 8
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑌 ⊆ ℂ) → ((abs ∘
− ) ↾ (𝑌
× 𝑌)) ∈
(∞Met‘𝑌)) |
38 | 33, 36, 37 | sylancr 587 |
. . . . . . 7
⊢ (𝑌 ⊆ ℝ → ((abs
∘ − ) ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌)) |
39 | 32, 38 | syl5eqel 2886 |
. . . . . 6
⊢ (𝑌 ⊆ ℝ → 𝑀 ∈ (∞Met‘𝑌)) |
40 | | xmetres2 22654 |
. . . . . . 7
⊢
(((ℝn‘1o) ∈
(∞Met‘(ℝ ↑𝑚 1o)) ∧
((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) ⊆ (ℝ
↑𝑚 1o)) →
((ℝn‘1o) ↾ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌))) ∈
(∞Met‘((𝑥
∈ ℝ ↦ ({∅} × {𝑥})) “ 𝑌))) |
41 | 17, 26, 40 | sylancr 587 |
. . . . . 6
⊢ (𝑌 ⊆ ℝ →
((ℝn‘1o) ↾ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌))) ∈
(∞Met‘((𝑥
∈ ℝ ↦ ({∅} × {𝑥})) “ 𝑌))) |
42 | | reheibor.3 |
. . . . . . 7
⊢ 𝑇 = (MetOpen‘𝑀) |
43 | 42, 28 | ismtyhmeo 34628 |
. . . . . 6
⊢ ((𝑀 ∈ (∞Met‘𝑌) ∧
((ℝn‘1o) ↾ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌))) ∈
(∞Met‘((𝑥
∈ ℝ ↦ ({∅} × {𝑥})) “ 𝑌))) → (𝑀 Ismty
((ℝn‘1o) ↾ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌)))) ⊆ (𝑇Homeo(MetOpen‘((ℝn‘1o)
↾ (((𝑥 ∈ ℝ ↦ ({∅}
× {𝑥})) “ 𝑌) × ((𝑥
∈ ℝ ↦ ({∅} × {𝑥}))
“ 𝑌)))))) |
44 | 39, 41, 43 | syl2anc 584 |
. . . . 5
⊢ (𝑌 ⊆ ℝ → (𝑀 Ismty
((ℝn‘1o) ↾ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌)))) ⊆ (𝑇Homeo(MetOpen‘((ℝn‘1o)
↾ (((𝑥 ∈ ℝ ↦ ({∅}
× {𝑥})) “ 𝑌) × ((𝑥
∈ ℝ ↦ ({∅} × {𝑥}))
“ 𝑌)))))) |
45 | 13 | a1i 11 |
. . . . . . 7
⊢ (𝑌 ⊆ ℝ → ((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ)) |
46 | 17 | a1i 11 |
. . . . . . 7
⊢ (𝑌 ⊆ ℝ →
(ℝn‘1o) ∈
(∞Met‘(ℝ ↑𝑚
1o))) |
47 | 12 | a1i 11 |
. . . . . . 7
⊢ (𝑌 ⊆ ℝ → (𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
∈ (((abs ∘ − ) ↾ (ℝ × ℝ)) Ismty
(ℝn‘1o))) |
48 | | eqid 2794 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) = ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) |
49 | | eqid 2794 |
. . . . . . . 8
⊢ (((abs
∘ − ) ↾ (ℝ × ℝ)) ↾ (𝑌 × 𝑌)) = (((abs ∘ − ) ↾
(ℝ × ℝ)) ↾ (𝑌 × 𝑌)) |
50 | 48, 49, 27 | ismtyres 34631 |
. . . . . . 7
⊢ (((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) ∧
(ℝn‘1o) ∈
(∞Met‘(ℝ ↑𝑚 1o))) ∧
((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
∈ (((abs ∘ − ) ↾ (ℝ × ℝ)) Ismty
(ℝn‘1o)) ∧ 𝑌 ⊆ ℝ)) → ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
↾ 𝑌) ∈ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ↾ (𝑌 × 𝑌)) Ismty
((ℝn‘1o) ↾ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌))))) |
51 | 45, 46, 47, 34, 50 | syl22anc 835 |
. . . . . 6
⊢ (𝑌 ⊆ ℝ → ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
↾ 𝑌) ∈ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ↾ (𝑌 × 𝑌)) Ismty
((ℝn‘1o) ↾ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌))))) |
52 | | xpss12 5461 |
. . . . . . . . . 10
⊢ ((𝑌 ⊆ ℝ ∧ 𝑌 ⊆ ℝ) → (𝑌 × 𝑌) ⊆ (ℝ ×
ℝ)) |
53 | 52 | anidms 567 |
. . . . . . . . 9
⊢ (𝑌 ⊆ ℝ → (𝑌 × 𝑌) ⊆ (ℝ ×
ℝ)) |
54 | 53 | resabs1d 5768 |
. . . . . . . 8
⊢ (𝑌 ⊆ ℝ → (((abs
∘ − ) ↾ (ℝ × ℝ)) ↾ (𝑌 × 𝑌)) = ((abs ∘ − ) ↾ (𝑌 × 𝑌))) |
55 | 54, 32 | syl6eqr 2848 |
. . . . . . 7
⊢ (𝑌 ⊆ ℝ → (((abs
∘ − ) ↾ (ℝ × ℝ)) ↾ (𝑌 × 𝑌)) = 𝑀) |
56 | 55 | oveq1d 7034 |
. . . . . 6
⊢ (𝑌 ⊆ ℝ → ((((abs
∘ − ) ↾ (ℝ × ℝ)) ↾ (𝑌 × 𝑌)) Ismty
((ℝn‘1o) ↾ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌)))) = (𝑀 Ismty
((ℝn‘1o) ↾ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌))))) |
57 | 51, 56 | eleqtrd 2884 |
. . . . 5
⊢ (𝑌 ⊆ ℝ → ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
↾ 𝑌) ∈ (𝑀 Ismty
((ℝn‘1o) ↾ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌))))) |
58 | 44, 57 | sseldd 3892 |
. . . 4
⊢ (𝑌 ⊆ ℝ → ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
↾ 𝑌) ∈ (𝑇Homeo(MetOpen‘((ℝn‘1o)
↾ (((𝑥 ∈ ℝ ↦ ({∅}
× {𝑥})) “ 𝑌) × ((𝑥
∈ ℝ ↦ ({∅} × {𝑥}))
“ 𝑌)))))) |
59 | | hmphi 22069 |
. . . 4
⊢ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
↾ 𝑌) ∈ (𝑇Homeo(MetOpen‘((ℝn‘1o)
↾ (((𝑥 ∈ ℝ ↦ ({∅}
× {𝑥})) “ 𝑌) × ((𝑥
∈ ℝ ↦ ({∅} × {𝑥}))
“ 𝑌))))) → 𝑇 ≃
(MetOpen‘((ℝn‘1o) ↾ (((𝑥 ∈ ℝ ↦ ({∅} × {𝑥})) “ 𝑌)
× ((𝑥 ∈ ℝ ↦ ({∅}
× {𝑥})) “ 𝑌))))) |
60 | 58, 59 | syl 17 |
. . 3
⊢ (𝑌 ⊆ ℝ → 𝑇 ≃
(MetOpen‘((ℝn‘1o) ↾
(((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌))))) |
61 | | cmphmph 22080 |
. . . 4
⊢ (𝑇 ≃
(MetOpen‘((ℝn‘1o) ↾
(((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌)))) → (𝑇 ∈ Comp →
(MetOpen‘((ℝn‘1o) ↾
(((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌)))) ∈
Comp)) |
62 | | hmphsym 22074 |
. . . . 5
⊢ (𝑇 ≃
(MetOpen‘((ℝn‘1o) ↾
(((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌)))) →
(MetOpen‘((ℝn‘1o) ↾
(((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌)))) ≃ 𝑇) |
63 | | cmphmph 22080 |
. . . . 5
⊢
((MetOpen‘((ℝn‘1o)
↾ (((𝑥 ∈ ℝ
↦ ({∅} × {𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌)))) ≃ 𝑇 →
((MetOpen‘((ℝn‘1o) ↾
(((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌)))) ∈ Comp
→ 𝑇 ∈
Comp)) |
64 | 62, 63 | syl 17 |
. . . 4
⊢ (𝑇 ≃
(MetOpen‘((ℝn‘1o) ↾
(((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌)))) →
((MetOpen‘((ℝn‘1o) ↾
(((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌)))) ∈ Comp
→ 𝑇 ∈
Comp)) |
65 | 61, 64 | impbid 213 |
. . 3
⊢ (𝑇 ≃
(MetOpen‘((ℝn‘1o) ↾
(((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌)))) → (𝑇 ∈ Comp ↔
(MetOpen‘((ℝn‘1o) ↾
(((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌)))) ∈
Comp)) |
66 | 60, 65 | syl 17 |
. 2
⊢ (𝑌 ⊆ ℝ → (𝑇 ∈ Comp ↔
(MetOpen‘((ℝn‘1o) ↾
(((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌)))) ∈
Comp)) |
67 | | reheibor.4 |
. . . . . . . 8
⊢ 𝑈 = (topGen‘ran
(,)) |
68 | | eqid 2794 |
. . . . . . . . 9
⊢
(MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) |
69 | 6, 68 | tgioo 23087 |
. . . . . . . 8
⊢
(topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾
(ℝ × ℝ))) |
70 | 67, 69 | eqtri 2818 |
. . . . . . 7
⊢ 𝑈 = (MetOpen‘((abs ∘
− ) ↾ (ℝ × ℝ))) |
71 | 70, 29 | ismtyhmeo 34628 |
. . . . . 6
⊢ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) ∧
(ℝn‘1o) ∈
(∞Met‘(ℝ ↑𝑚 1o))) →
(((abs ∘ − ) ↾ (ℝ × ℝ)) Ismty
(ℝn‘1o)) ⊆ (𝑈Homeo(MetOpen‘(ℝn‘1o)))) |
72 | 13, 17, 71 | mp2an 688 |
. . . . 5
⊢ (((abs
∘ − ) ↾ (ℝ × ℝ)) Ismty
(ℝn‘1o)) ⊆ (𝑈Homeo(MetOpen‘(ℝn‘1o))) |
73 | 72, 12 | sselii 3888 |
. . . 4
⊢ (𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
∈ (𝑈Homeo(MetOpen‘(ℝn‘1o))) |
74 | | retopon 23055 |
. . . . . . 7
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
75 | 67, 74 | eqeltri 2878 |
. . . . . 6
⊢ 𝑈 ∈
(TopOn‘ℝ) |
76 | 75 | toponunii 21208 |
. . . . 5
⊢ ℝ =
∪ 𝑈 |
77 | 76 | hmeocld 22059 |
. . . 4
⊢ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
∈ (𝑈Homeo(MetOpen‘(ℝn‘1o)))
∧ 𝑌 ⊆ ℝ) → (𝑌 ∈ (Clsd‘𝑈) ↔ ((𝑥
∈ ℝ ↦ ({∅} × {𝑥}))
“ 𝑌) ∈
(Clsd‘(MetOpen‘(ℝn‘1o))))) |
78 | 73, 34, 77 | sylancr 587 |
. . 3
⊢ (𝑌 ⊆ ℝ → (𝑌 ∈ (Clsd‘𝑈) ↔ ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) ∈
(Clsd‘(MetOpen‘(ℝn‘1o))))) |
79 | | ismtybnd 34630 |
. . . 4
⊢ ((𝑀 ∈ (∞Met‘𝑌) ∧
((ℝn‘1o) ↾ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌))) ∈
(∞Met‘((𝑥
∈ ℝ ↦ ({∅} × {𝑥})) “ 𝑌)) ∧ ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) ↾ 𝑌) ∈ (𝑀 Ismty
((ℝn‘1o) ↾ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌))))) → (𝑀 ∈ (Bnd‘𝑌) ↔
((ℝn‘1o) ↾ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌))) ∈ (Bnd‘((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌)))) |
80 | 39, 41, 57, 79 | syl3anc 1364 |
. . 3
⊢ (𝑌 ⊆ ℝ → (𝑀 ∈ (Bnd‘𝑌) ↔
((ℝn‘1o) ↾ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌))) ∈ (Bnd‘((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌)))) |
81 | 78, 80 | anbi12d 630 |
. 2
⊢ (𝑌 ⊆ ℝ → ((𝑌 ∈ (Clsd‘𝑈) ∧ 𝑀 ∈ (Bnd‘𝑌)) ↔ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) ∈
(Clsd‘(MetOpen‘(ℝn‘1o)))
∧ ((ℝn‘1o) ↾ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌))) ∈
(Bnd‘((𝑥 ∈
ℝ ↦ ({∅} × {𝑥})) “ 𝑌))))) |
82 | 31, 66, 81 | 3bitr4d 312 |
1
⊢ (𝑌 ⊆ ℝ → (𝑇 ∈ Comp ↔ (𝑌 ∈ (Clsd‘𝑈) ∧ 𝑀 ∈ (Bnd‘𝑌)))) |