Step | Hyp | Ref
| Expression |
1 | | df1o2 7572 |
. . . 4
⊢
1𝑜 = {∅} |
2 | | snfi 8038 |
. . . 4
⊢ {∅}
∈ Fin |
3 | 1, 2 | eqeltri 2697 |
. . 3
⊢
1𝑜 ∈ Fin |
4 | | imassrn 5477 |
. . . . 5
⊢ ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) ⊆ ran
(𝑥 ∈ ℝ ↦
({∅} × {𝑥})) |
5 | | 0ex 4790 |
. . . . . . . . . 10
⊢ ∅
∈ V |
6 | | eqid 2622 |
. . . . . . . . . . 11
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − )
↾ (ℝ × ℝ)) |
7 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ ↦
({∅} × {𝑥})) =
(𝑥 ∈ ℝ ↦
({∅} × {𝑥})) |
8 | 6, 7 | ismrer1 33637 |
. . . . . . . . . 10
⊢ (∅
∈ V → (𝑥 ∈
ℝ ↦ ({∅} × {𝑥})) ∈ (((abs ∘ − ) ↾
(ℝ × ℝ)) Ismty
(ℝn‘{∅}))) |
9 | 5, 8 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
∈ (((abs ∘ − ) ↾ (ℝ × ℝ)) Ismty
(ℝn‘{∅})) |
10 | 1 | fveq2i 6194 |
. . . . . . . . . 10
⊢
(ℝn‘1𝑜) =
(ℝn‘{∅}) |
11 | 10 | oveq2i 6661 |
. . . . . . . . 9
⊢ (((abs
∘ − ) ↾ (ℝ × ℝ)) Ismty
(ℝn‘1𝑜)) = (((abs ∘
− ) ↾ (ℝ × ℝ)) Ismty
(ℝn‘{∅})) |
12 | 9, 11 | eleqtrri 2700 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
∈ (((abs ∘ − ) ↾ (ℝ × ℝ)) Ismty
(ℝn‘1𝑜)) |
13 | 6 | rexmet 22594 |
. . . . . . . . 9
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) |
14 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (ℝ
↑𝑚 1𝑜) = (ℝ
↑𝑚 1𝑜) |
15 | 14 | rrnmet 33628 |
. . . . . . . . . 10
⊢
(1𝑜 ∈ Fin →
(ℝn‘1𝑜) ∈
(Met‘(ℝ ↑𝑚
1𝑜))) |
16 | | metxmet 22139 |
. . . . . . . . . 10
⊢
((ℝn‘1𝑜) ∈
(Met‘(ℝ ↑𝑚 1𝑜)) →
(ℝn‘1𝑜) ∈
(∞Met‘(ℝ ↑𝑚
1𝑜))) |
17 | 3, 15, 16 | mp2b 10 |
. . . . . . . . 9
⊢
(ℝn‘1𝑜) ∈
(∞Met‘(ℝ ↑𝑚
1𝑜)) |
18 | | isismty 33600 |
. . . . . . . . 9
⊢ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) ∧
(ℝn‘1𝑜) ∈
(∞Met‘(ℝ ↑𝑚 1𝑜)))
→ ((𝑥 ∈ ℝ
↦ ({∅} × {𝑥})) ∈ (((abs ∘ − ) ↾
(ℝ × ℝ)) Ismty
(ℝn‘1𝑜)) ↔ ((𝑥 ∈ ℝ ↦
({∅} × {𝑥})):ℝ–1-1-onto→(ℝ ↑𝑚
1𝑜) ∧ ∀𝑦 ∈ ℝ ∀𝑧 ∈ ℝ (𝑦((abs ∘ − ) ↾ (ℝ
× ℝ))𝑧) =
(((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))‘𝑦)(ℝn‘1𝑜)((𝑥 ∈ ℝ ↦ ({∅} × {𝑥}))‘𝑧))))) |
19 | 13, 17, 18 | mp2an 708 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
∈ (((abs ∘ − ) ↾ (ℝ × ℝ)) Ismty
(ℝn‘1𝑜)) ↔ ((𝑥 ∈ ℝ ↦
({∅} × {𝑥})):ℝ–1-1-onto→(ℝ ↑𝑚
1𝑜) ∧ ∀𝑦 ∈ ℝ ∀𝑧 ∈ ℝ (𝑦((abs ∘ − ) ↾ (ℝ
× ℝ))𝑧) =
(((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))‘𝑦)(ℝn‘1𝑜)((𝑥 ∈ ℝ ↦ ({∅} × {𝑥}))‘𝑧)))) |
20 | 12, 19 | mpbi 220 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ↦
({∅} × {𝑥})):ℝ–1-1-onto→(ℝ ↑𝑚
1𝑜) ∧ ∀𝑦 ∈ ℝ ∀𝑧 ∈ ℝ (𝑦((abs ∘ − ) ↾ (ℝ
× ℝ))𝑧) =
(((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))‘𝑦)(ℝn‘1𝑜)((𝑥 ∈ ℝ ↦ ({∅} × {𝑥}))‘𝑧))) |
21 | 20 | simpli 474 |
. . . . . 6
⊢ (𝑥 ∈ ℝ ↦
({∅} × {𝑥})):ℝ–1-1-onto→(ℝ ↑𝑚
1𝑜) |
22 | | f1of 6137 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ↦
({∅} × {𝑥})):ℝ–1-1-onto→(ℝ ↑𝑚
1𝑜) → (𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})):ℝ⟶(ℝ
↑𝑚 1𝑜)) |
23 | | frn 6053 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ↦
({∅} × {𝑥})):ℝ⟶(ℝ
↑𝑚 1𝑜) → ran (𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
⊆ (ℝ ↑𝑚
1𝑜)) |
24 | 21, 22, 23 | mp2b 10 |
. . . . 5
⊢ ran
(𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
⊆ (ℝ ↑𝑚
1𝑜) |
25 | 4, 24 | sstri 3612 |
. . . 4
⊢ ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) ⊆ (ℝ
↑𝑚 1𝑜) |
26 | 25 | a1i 11 |
. . 3
⊢ (𝑌 ⊆ ℝ → ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) ⊆ (ℝ
↑𝑚 1𝑜)) |
27 | | eqid 2622 |
. . . 4
⊢
((ℝn‘1𝑜) ↾
(((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌))) =
((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌))) |
28 | | eqid 2622 |
. . . 4
⊢
(MetOpen‘((ℝn‘1𝑜)
↾ (((𝑥 ∈ ℝ
↦ ({∅} × {𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌)))) =
(MetOpen‘((ℝn‘1𝑜)
↾ (((𝑥 ∈ ℝ
↦ ({∅} × {𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌)))) |
29 | | eqid 2622 |
. . . 4
⊢
(MetOpen‘(ℝn‘1𝑜))
=
(MetOpen‘(ℝn‘1𝑜)) |
30 | 14, 27, 28, 29 | rrnheibor 33636 |
. . 3
⊢
((1𝑜 ∈ Fin ∧ ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) ⊆ (ℝ
↑𝑚 1𝑜)) →
((MetOpen‘((ℝn‘1𝑜)
↾ (((𝑥 ∈ ℝ
↦ ({∅} × {𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌)))) ∈ Comp ↔ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) ∈
(Clsd‘(MetOpen‘(ℝn‘1𝑜)))
∧ ((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦ ({∅}
× {𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} × {𝑥})) “ 𝑌))) ∈ (Bnd‘((𝑥 ∈ ℝ ↦ ({∅} × {𝑥})) “ 𝑌))))) |
31 | 3, 26, 30 | sylancr 695 |
. 2
⊢ (𝑌 ⊆ ℝ →
((MetOpen‘((ℝn‘1𝑜)
↾ (((𝑥 ∈ ℝ
↦ ({∅} × {𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌)))) ∈ Comp ↔ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) ∈
(Clsd‘(MetOpen‘(ℝn‘1𝑜)))
∧ ((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦ ({∅}
× {𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} × {𝑥})) “ 𝑌))) ∈ (Bnd‘((𝑥 ∈ ℝ ↦ ({∅} × {𝑥})) “ 𝑌))))) |
32 | | reheibor.2 |
. . . . . . 7
⊢ 𝑀 = ((abs ∘ − )
↾ (𝑌 × 𝑌)) |
33 | | cnxmet 22576 |
. . . . . . . 8
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
34 | | id 22 |
. . . . . . . . 9
⊢ (𝑌 ⊆ ℝ → 𝑌 ⊆
ℝ) |
35 | | ax-resscn 9993 |
. . . . . . . . 9
⊢ ℝ
⊆ ℂ |
36 | 34, 35 | syl6ss 3615 |
. . . . . . . 8
⊢ (𝑌 ⊆ ℝ → 𝑌 ⊆
ℂ) |
37 | | xmetres2 22166 |
. . . . . . . 8
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑌 ⊆ ℂ) → ((abs ∘
− ) ↾ (𝑌
× 𝑌)) ∈
(∞Met‘𝑌)) |
38 | 33, 36, 37 | sylancr 695 |
. . . . . . 7
⊢ (𝑌 ⊆ ℝ → ((abs
∘ − ) ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌)) |
39 | 32, 38 | syl5eqel 2705 |
. . . . . 6
⊢ (𝑌 ⊆ ℝ → 𝑀 ∈ (∞Met‘𝑌)) |
40 | | xmetres2 22166 |
. . . . . . 7
⊢
(((ℝn‘1𝑜) ∈
(∞Met‘(ℝ ↑𝑚 1𝑜))
∧ ((𝑥 ∈ ℝ
↦ ({∅} × {𝑥})) “ 𝑌) ⊆ (ℝ
↑𝑚 1𝑜)) →
((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌))) ∈
(∞Met‘((𝑥
∈ ℝ ↦ ({∅} × {𝑥})) “ 𝑌))) |
41 | 17, 26, 40 | sylancr 695 |
. . . . . 6
⊢ (𝑌 ⊆ ℝ →
((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌))) ∈
(∞Met‘((𝑥
∈ ℝ ↦ ({∅} × {𝑥})) “ 𝑌))) |
42 | | reheibor.3 |
. . . . . . 7
⊢ 𝑇 = (MetOpen‘𝑀) |
43 | 42, 28 | ismtyhmeo 33604 |
. . . . . 6
⊢ ((𝑀 ∈ (∞Met‘𝑌) ∧
((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌))) ∈
(∞Met‘((𝑥
∈ ℝ ↦ ({∅} × {𝑥})) “ 𝑌))) → (𝑀 Ismty
((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌)))) ⊆
(𝑇Homeo(MetOpen‘((ℝn‘1𝑜)
↾ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) × ((𝑥 ∈
ℝ ↦ ({∅} × {𝑥})) “ 𝑌)))))) |
44 | 39, 41, 43 | syl2anc 693 |
. . . . 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 2622 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) = ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) |
49 | | eqid 2622 |
. . . . . . . 8
⊢ (((abs
∘ − ) ↾ (ℝ × ℝ)) ↾ (𝑌 × 𝑌)) = (((abs ∘ − ) ↾
(ℝ × ℝ)) ↾ (𝑌 × 𝑌)) |
50 | 48, 49, 27 | ismtyres 33607 |
. . . . . . 7
⊢ (((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) ∧
(ℝn‘1𝑜) ∈
(∞Met‘(ℝ ↑𝑚 1𝑜)))
∧ ((𝑥 ∈ ℝ
↦ ({∅} × {𝑥})) ∈ (((abs ∘ − ) ↾
(ℝ × ℝ)) Ismty
(ℝn‘1𝑜)) ∧ 𝑌 ⊆ ℝ)) →
((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
↾ 𝑌) ∈ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ↾ (𝑌 × 𝑌)) Ismty
((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌))))) |
51 | 45, 46, 47, 34, 50 | syl22anc 1327 |
. . . . . 6
⊢ (𝑌 ⊆ ℝ → ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
↾ 𝑌) ∈ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ↾ (𝑌 × 𝑌)) Ismty
((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌))))) |
52 | | xpss12 5225 |
. . . . . . . . . 10
⊢ ((𝑌 ⊆ ℝ ∧ 𝑌 ⊆ ℝ) → (𝑌 × 𝑌) ⊆ (ℝ ×
ℝ)) |
53 | 52 | anidms 677 |
. . . . . . . . 9
⊢ (𝑌 ⊆ ℝ → (𝑌 × 𝑌) ⊆ (ℝ ×
ℝ)) |
54 | 53 | resabs1d 5428 |
. . . . . . . 8
⊢ (𝑌 ⊆ ℝ → (((abs
∘ − ) ↾ (ℝ × ℝ)) ↾ (𝑌 × 𝑌)) = ((abs ∘ − ) ↾ (𝑌 × 𝑌))) |
55 | 54, 32 | syl6eqr 2674 |
. . . . . . 7
⊢ (𝑌 ⊆ ℝ → (((abs
∘ − ) ↾ (ℝ × ℝ)) ↾ (𝑌 × 𝑌)) = 𝑀) |
56 | 55 | oveq1d 6665 |
. . . . . 6
⊢ (𝑌 ⊆ ℝ → ((((abs
∘ − ) ↾ (ℝ × ℝ)) ↾ (𝑌 × 𝑌)) Ismty
((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌)))) = (𝑀 Ismty
((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌))))) |
57 | 51, 56 | eleqtrd 2703 |
. . . . 5
⊢ (𝑌 ⊆ ℝ → ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
↾ 𝑌) ∈ (𝑀 Ismty
((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌))))) |
58 | 44, 57 | sseldd 3604 |
. . . 4
⊢ (𝑌 ⊆ ℝ → ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
↾ 𝑌) ∈ (𝑇Homeo(MetOpen‘((ℝn‘1𝑜)
↾ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) × ((𝑥 ∈
ℝ ↦ ({∅} × {𝑥})) “ 𝑌)))))) |
59 | | hmphi 21580 |
. . . 4
⊢ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
↾ 𝑌) ∈ (𝑇Homeo(MetOpen‘((ℝn‘1𝑜)
↾ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) × ((𝑥 ∈
ℝ ↦ ({∅} × {𝑥})) “ 𝑌))))) → 𝑇 ≃
(MetOpen‘((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦ ({∅} × {𝑥})) “ 𝑌) ×
((𝑥 ∈ ℝ ↦ ({∅} × {𝑥})) “ 𝑌))))) |
60 | 58, 59 | syl 17 |
. . 3
⊢ (𝑌 ⊆ ℝ → 𝑇 ≃
(MetOpen‘((ℝn‘1𝑜)
↾ (((𝑥 ∈ ℝ
↦ ({∅} × {𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌))))) |
61 | | cmphmph 21591 |
. . . 4
⊢ (𝑇 ≃
(MetOpen‘((ℝn‘1𝑜)
↾ (((𝑥 ∈ ℝ
↦ ({∅} × {𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌)))) → (𝑇 ∈ Comp →
(MetOpen‘((ℝn‘1𝑜)
↾ (((𝑥 ∈ ℝ
↦ ({∅} × {𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌)))) ∈
Comp)) |
62 | | hmphsym 21585 |
. . . . 5
⊢ (𝑇 ≃
(MetOpen‘((ℝn‘1𝑜)
↾ (((𝑥 ∈ ℝ
↦ ({∅} × {𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌)))) →
(MetOpen‘((ℝn‘1𝑜)
↾ (((𝑥 ∈ ℝ
↦ ({∅} × {𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌)))) ≃ 𝑇) |
63 | | cmphmph 21591 |
. . . . 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 202 |
. . 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 2622 |
. . . . . . . . 9
⊢
(MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) |
69 | 6, 68 | tgioo 22599 |
. . . . . . . 8
⊢
(topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾
(ℝ × ℝ))) |
70 | 67, 69 | eqtri 2644 |
. . . . . . 7
⊢ 𝑈 = (MetOpen‘((abs ∘
− ) ↾ (ℝ × ℝ))) |
71 | 70, 29 | ismtyhmeo 33604 |
. . . . . 6
⊢ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) ∧
(ℝn‘1𝑜) ∈
(∞Met‘(ℝ ↑𝑚 1𝑜)))
→ (((abs ∘ − ) ↾ (ℝ × ℝ)) Ismty
(ℝn‘1𝑜)) ⊆ (𝑈Homeo(MetOpen‘(ℝn‘1𝑜)))) |
72 | 13, 17, 71 | mp2an 708 |
. . . . 5
⊢ (((abs
∘ − ) ↾ (ℝ × ℝ)) Ismty
(ℝn‘1𝑜)) ⊆ (𝑈Homeo(MetOpen‘(ℝn‘1𝑜))) |
73 | 72, 12 | sselii 3600 |
. . . 4
⊢ (𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
∈ (𝑈Homeo(MetOpen‘(ℝn‘1𝑜))) |
74 | | retopon 22567 |
. . . . . . 7
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
75 | 67, 74 | eqeltri 2697 |
. . . . . 6
⊢ 𝑈 ∈
(TopOn‘ℝ) |
76 | 75 | toponunii 20721 |
. . . . 5
⊢ ℝ =
∪ 𝑈 |
77 | 76 | hmeocld 21570 |
. . . 4
⊢ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
∈ (𝑈Homeo(MetOpen‘(ℝn‘1𝑜)))
∧ 𝑌 ⊆ ℝ) → (𝑌 ∈ (Clsd‘𝑈)
↔ ((𝑥 ∈ ℝ ↦ ({∅} × {𝑥})) “ 𝑌)
∈ (Clsd‘(MetOpen‘(ℝn‘1𝑜))))) |
78 | 73, 34, 77 | sylancr 695 |
. . 3
⊢ (𝑌 ⊆ ℝ → (𝑌 ∈ (Clsd‘𝑈) ↔ ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) ∈
(Clsd‘(MetOpen‘(ℝn‘1𝑜))))) |
79 | | ismtybnd 33606 |
. . . 4
⊢ ((𝑀 ∈ (∞Met‘𝑌) ∧
((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌))) ∈
(∞Met‘((𝑥
∈ ℝ ↦ ({∅} × {𝑥})) “ 𝑌)) ∧ ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) ↾ 𝑌) ∈ (𝑀 Ismty
((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌))))) →
(𝑀 ∈ (Bnd‘𝑌) ↔
((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌))) ∈
(Bnd‘((𝑥 ∈
ℝ ↦ ({∅} × {𝑥})) “ 𝑌)))) |
80 | 39, 41, 57, 79 | syl3anc 1326 |
. . 3
⊢ (𝑌 ⊆ ℝ → (𝑀 ∈ (Bnd‘𝑌) ↔
((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌))) ∈
(Bnd‘((𝑥 ∈
ℝ ↦ ({∅} × {𝑥})) “ 𝑌)))) |
81 | 78, 80 | anbi12d 747 |
. 2
⊢ (𝑌 ⊆ ℝ → ((𝑌 ∈ (Clsd‘𝑈) ∧ 𝑀 ∈ (Bnd‘𝑌)) ↔ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) ∈
(Clsd‘(MetOpen‘(ℝn‘1𝑜)))
∧ ((ℝn‘1𝑜) ↾ (((𝑥 ∈ ℝ ↦ ({∅}
× {𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} × {𝑥})) “ 𝑌))) ∈ (Bnd‘((𝑥 ∈ ℝ ↦ ({∅} × {𝑥})) “ 𝑌))))) |
82 | 31, 66, 81 | 3bitr4d 300 |
1
⊢ (𝑌 ⊆ ℝ → (𝑇 ∈ Comp ↔ (𝑌 ∈ (Clsd‘𝑈) ∧ 𝑀 ∈ (Bnd‘𝑌)))) |