| Step | Hyp | Ref
| Expression |
| 1 | | df1o2 8513 |
. . . 4
⊢
1o = {∅} |
| 2 | | snfi 9083 |
. . . 4
⊢ {∅}
∈ Fin |
| 3 | 1, 2 | eqeltri 2837 |
. . 3
⊢
1o ∈ Fin |
| 4 | | imassrn 6089 |
. . . . 5
⊢ ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) ⊆ ran
(𝑥 ∈ ℝ ↦
({∅} × {𝑥})) |
| 5 | | 0ex 5307 |
. . . . . . . . . 10
⊢ ∅
∈ V |
| 6 | | eqid 2737 |
. . . . . . . . . . 11
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − )
↾ (ℝ × ℝ)) |
| 7 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ ↦
({∅} × {𝑥})) =
(𝑥 ∈ ℝ ↦
({∅} × {𝑥})) |
| 8 | 6, 7 | ismrer1 37845 |
. . . . . . . . . 10
⊢ (∅
∈ V → (𝑥 ∈
ℝ ↦ ({∅} × {𝑥})) ∈ (((abs ∘ − ) ↾
(ℝ × ℝ)) Ismty
(ℝn‘{∅}))) |
| 9 | 5, 8 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
∈ (((abs ∘ − ) ↾ (ℝ × ℝ)) Ismty
(ℝn‘{∅})) |
| 10 | 1 | fveq2i 6909 |
. . . . . . . . . 10
⊢
(ℝn‘1o) =
(ℝn‘{∅}) |
| 11 | 10 | oveq2i 7442 |
. . . . . . . . 9
⊢ (((abs
∘ − ) ↾ (ℝ × ℝ)) Ismty
(ℝn‘1o)) = (((abs ∘ − )
↾ (ℝ × ℝ)) Ismty
(ℝn‘{∅})) |
| 12 | 9, 11 | eleqtrri 2840 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
∈ (((abs ∘ − ) ↾ (ℝ × ℝ)) Ismty
(ℝn‘1o)) |
| 13 | 6 | rexmet 24812 |
. . . . . . . . 9
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) |
| 14 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (ℝ
↑m 1o) = (ℝ ↑m
1o) |
| 15 | 14 | rrnmet 37836 |
. . . . . . . . . 10
⊢
(1o ∈ Fin →
(ℝn‘1o) ∈ (Met‘(ℝ
↑m 1o))) |
| 16 | | metxmet 24344 |
. . . . . . . . . 10
⊢
((ℝn‘1o) ∈
(Met‘(ℝ ↑m 1o)) →
(ℝn‘1o) ∈
(∞Met‘(ℝ ↑m 1o))) |
| 17 | 3, 15, 16 | mp2b 10 |
. . . . . . . . 9
⊢
(ℝn‘1o) ∈
(∞Met‘(ℝ ↑m 1o)) |
| 18 | | isismty 37808 |
. . . . . . . . 9
⊢ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) ∧
(ℝn‘1o) ∈
(∞Met‘(ℝ ↑m 1o))) → ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
∈ (((abs ∘ − ) ↾ (ℝ × ℝ)) Ismty
(ℝn‘1o)) ↔ ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})):ℝ–1-1-onto→(ℝ ↑m 1o)
∧ ∀𝑦 ∈
ℝ ∀𝑧 ∈
ℝ (𝑦((abs ∘
− ) ↾ (ℝ × ℝ))𝑧) = (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥}))‘𝑦)(ℝn‘1o)((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥}))‘𝑧))))) |
| 19 | 13, 17, 18 | mp2an 692 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
∈ (((abs ∘ − ) ↾ (ℝ × ℝ)) Ismty
(ℝn‘1o)) ↔ ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})):ℝ–1-1-onto→(ℝ ↑m 1o)
∧ ∀𝑦 ∈
ℝ ∀𝑧 ∈
ℝ (𝑦((abs ∘
− ) ↾ (ℝ × ℝ))𝑧) = (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥}))‘𝑦)(ℝn‘1o)((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥}))‘𝑧)))) |
| 20 | 12, 19 | mpbi 230 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ↦
({∅} × {𝑥})):ℝ–1-1-onto→(ℝ ↑m 1o)
∧ ∀𝑦 ∈
ℝ ∀𝑧 ∈
ℝ (𝑦((abs ∘
− ) ↾ (ℝ × ℝ))𝑧) = (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥}))‘𝑦)(ℝn‘1o)((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥}))‘𝑧))) |
| 21 | 20 | simpli 483 |
. . . . . 6
⊢ (𝑥 ∈ ℝ ↦
({∅} × {𝑥})):ℝ–1-1-onto→(ℝ ↑m
1o) |
| 22 | | f1of 6848 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ↦
({∅} × {𝑥})):ℝ–1-1-onto→(ℝ ↑m 1o)
→ (𝑥 ∈ ℝ
↦ ({∅} × {𝑥})):ℝ⟶(ℝ
↑m 1o)) |
| 23 | | frn 6743 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ↦
({∅} × {𝑥})):ℝ⟶(ℝ
↑m 1o) → ran (𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) ⊆ (ℝ
↑m 1o)) |
| 24 | 21, 22, 23 | mp2b 10 |
. . . . 5
⊢ ran
(𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
⊆ (ℝ ↑m 1o) |
| 25 | 4, 24 | sstri 3993 |
. . . 4
⊢ ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) ⊆ (ℝ
↑m 1o) |
| 26 | 25 | a1i 11 |
. . 3
⊢ (𝑌 ⊆ ℝ → ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) ⊆ (ℝ
↑m 1o)) |
| 27 | | eqid 2737 |
. . . 4
⊢
((ℝn‘1o) ↾ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌))) =
((ℝn‘1o) ↾ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌))) |
| 28 | | eqid 2737 |
. . . 4
⊢
(MetOpen‘((ℝn‘1o) ↾
(((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌)))) =
(MetOpen‘((ℝn‘1o) ↾
(((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌)))) |
| 29 | | eqid 2737 |
. . . 4
⊢
(MetOpen‘(ℝn‘1o)) =
(MetOpen‘(ℝn‘1o)) |
| 30 | 14, 27, 28, 29 | rrnheibor 37844 |
. . 3
⊢
((1o ∈ Fin ∧ ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) ⊆ (ℝ
↑m 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 24793 |
. . . . . . . 8
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
| 34 | | id 22 |
. . . . . . . . 9
⊢ (𝑌 ⊆ ℝ → 𝑌 ⊆
ℝ) |
| 35 | | ax-resscn 11212 |
. . . . . . . . 9
⊢ ℝ
⊆ ℂ |
| 36 | 34, 35 | sstrdi 3996 |
. . . . . . . 8
⊢ (𝑌 ⊆ ℝ → 𝑌 ⊆
ℂ) |
| 37 | | xmetres2 24371 |
. . . . . . . 8
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑌 ⊆ ℂ) → ((abs ∘
− ) ↾ (𝑌
× 𝑌)) ∈
(∞Met‘𝑌)) |
| 38 | 33, 36, 37 | sylancr 587 |
. . . . . . 7
⊢ (𝑌 ⊆ ℝ → ((abs
∘ − ) ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌)) |
| 39 | 32, 38 | eqeltrid 2845 |
. . . . . 6
⊢ (𝑌 ⊆ ℝ → 𝑀 ∈ (∞Met‘𝑌)) |
| 40 | | xmetres2 24371 |
. . . . . . 7
⊢
(((ℝn‘1o) ∈
(∞Met‘(ℝ ↑m 1o)) ∧ ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) ⊆ (ℝ
↑m 1o)) →
((ℝn‘1o) ↾ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌))) ∈
(∞Met‘((𝑥
∈ ℝ ↦ ({∅} × {𝑥})) “ 𝑌))) |
| 41 | 17, 26, 40 | sylancr 587 |
. . . . . 6
⊢ (𝑌 ⊆ ℝ →
((ℝn‘1o) ↾ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌))) ∈
(∞Met‘((𝑥
∈ ℝ ↦ ({∅} × {𝑥})) “ 𝑌))) |
| 42 | | reheibor.3 |
. . . . . . 7
⊢ 𝑇 = (MetOpen‘𝑀) |
| 43 | 42, 28 | ismtyhmeo 37812 |
. . . . . 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‘(ℝ ↑m 1o))) |
| 47 | 12 | a1i 11 |
. . . . . . 7
⊢ (𝑌 ⊆ ℝ → (𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
∈ (((abs ∘ − ) ↾ (ℝ × ℝ)) Ismty
(ℝn‘1o))) |
| 48 | | eqid 2737 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) = ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) |
| 49 | | eqid 2737 |
. . . . . . . 8
⊢ (((abs
∘ − ) ↾ (ℝ × ℝ)) ↾ (𝑌 × 𝑌)) = (((abs ∘ − ) ↾
(ℝ × ℝ)) ↾ (𝑌 × 𝑌)) |
| 50 | 48, 49, 27 | ismtyres 37815 |
. . . . . . 7
⊢ (((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) ∧
(ℝn‘1o) ∈
(∞Met‘(ℝ ↑m 1o))) ∧ ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
∈ (((abs ∘ − ) ↾ (ℝ × ℝ)) Ismty
(ℝn‘1o)) ∧ 𝑌 ⊆ ℝ)) → ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
↾ 𝑌) ∈ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ↾ (𝑌 × 𝑌)) Ismty
((ℝn‘1o) ↾ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌))))) |
| 51 | 45, 46, 47, 34, 50 | syl22anc 839 |
. . . . . 6
⊢ (𝑌 ⊆ ℝ → ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
↾ 𝑌) ∈ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ↾ (𝑌 × 𝑌)) Ismty
((ℝn‘1o) ↾ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌))))) |
| 52 | | xpss12 5700 |
. . . . . . . . . 10
⊢ ((𝑌 ⊆ ℝ ∧ 𝑌 ⊆ ℝ) → (𝑌 × 𝑌) ⊆ (ℝ ×
ℝ)) |
| 53 | 52 | anidms 566 |
. . . . . . . . 9
⊢ (𝑌 ⊆ ℝ → (𝑌 × 𝑌) ⊆ (ℝ ×
ℝ)) |
| 54 | 53 | resabs1d 6026 |
. . . . . . . 8
⊢ (𝑌 ⊆ ℝ → (((abs
∘ − ) ↾ (ℝ × ℝ)) ↾ (𝑌 × 𝑌)) = ((abs ∘ − ) ↾ (𝑌 × 𝑌))) |
| 55 | 54, 32 | eqtr4di 2795 |
. . . . . . 7
⊢ (𝑌 ⊆ ℝ → (((abs
∘ − ) ↾ (ℝ × ℝ)) ↾ (𝑌 × 𝑌)) = 𝑀) |
| 56 | 55 | oveq1d 7446 |
. . . . . 6
⊢ (𝑌 ⊆ ℝ → ((((abs
∘ − ) ↾ (ℝ × ℝ)) ↾ (𝑌 × 𝑌)) Ismty
((ℝn‘1o) ↾ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌)))) = (𝑀 Ismty
((ℝn‘1o) ↾ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌))))) |
| 57 | 51, 56 | eleqtrd 2843 |
. . . . 5
⊢ (𝑌 ⊆ ℝ → ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
↾ 𝑌) ∈ (𝑀 Ismty
((ℝn‘1o) ↾ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌))))) |
| 58 | 44, 57 | sseldd 3984 |
. . . 4
⊢ (𝑌 ⊆ ℝ → ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
↾ 𝑌) ∈ (𝑇Homeo(MetOpen‘((ℝn‘1o)
↾ (((𝑥 ∈ ℝ ↦ ({∅}
× {𝑥})) “ 𝑌) × ((𝑥
∈ ℝ ↦ ({∅} × {𝑥}))
“ 𝑌)))))) |
| 59 | | hmphi 23785 |
. . . 4
⊢ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
↾ 𝑌) ∈ (𝑇Homeo(MetOpen‘((ℝn‘1o)
↾ (((𝑥 ∈ ℝ ↦ ({∅}
× {𝑥})) “ 𝑌) × ((𝑥
∈ ℝ ↦ ({∅} × {𝑥}))
“ 𝑌))))) → 𝑇 ≃
(MetOpen‘((ℝn‘1o) ↾ (((𝑥 ∈ ℝ ↦ ({∅} × {𝑥})) “ 𝑌)
× ((𝑥 ∈ ℝ ↦ ({∅}
× {𝑥})) “ 𝑌))))) |
| 60 | 58, 59 | syl 17 |
. . 3
⊢ (𝑌 ⊆ ℝ → 𝑇 ≃
(MetOpen‘((ℝn‘1o) ↾
(((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌))))) |
| 61 | | cmphmph 23796 |
. . . 4
⊢ (𝑇 ≃
(MetOpen‘((ℝn‘1o) ↾
(((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌)))) → (𝑇 ∈ Comp →
(MetOpen‘((ℝn‘1o) ↾
(((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌)))) ∈
Comp)) |
| 62 | | hmphsym 23790 |
. . . . 5
⊢ (𝑇 ≃
(MetOpen‘((ℝn‘1o) ↾
(((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌)))) →
(MetOpen‘((ℝn‘1o) ↾
(((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌)))) ≃ 𝑇) |
| 63 | | cmphmph 23796 |
. . . . 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 212 |
. . 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 2737 |
. . . . . . . . 9
⊢
(MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) |
| 69 | 6, 68 | tgioo 24817 |
. . . . . . . 8
⊢
(topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾
(ℝ × ℝ))) |
| 70 | 67, 69 | eqtri 2765 |
. . . . . . 7
⊢ 𝑈 = (MetOpen‘((abs ∘
− ) ↾ (ℝ × ℝ))) |
| 71 | 70, 29 | ismtyhmeo 37812 |
. . . . . 6
⊢ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) ∧
(ℝn‘1o) ∈
(∞Met‘(ℝ ↑m 1o))) → (((abs
∘ − ) ↾ (ℝ × ℝ)) Ismty
(ℝn‘1o)) ⊆ (𝑈Homeo(MetOpen‘(ℝn‘1o)))) |
| 72 | 13, 17, 71 | mp2an 692 |
. . . . 5
⊢ (((abs
∘ − ) ↾ (ℝ × ℝ)) Ismty
(ℝn‘1o)) ⊆ (𝑈Homeo(MetOpen‘(ℝn‘1o))) |
| 73 | 72, 12 | sselii 3980 |
. . . 4
⊢ (𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
∈ (𝑈Homeo(MetOpen‘(ℝn‘1o))) |
| 74 | | retopon 24784 |
. . . . . . 7
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
| 75 | 67, 74 | eqeltri 2837 |
. . . . . 6
⊢ 𝑈 ∈
(TopOn‘ℝ) |
| 76 | 75 | toponunii 22922 |
. . . . 5
⊢ ℝ =
∪ 𝑈 |
| 77 | 76 | hmeocld 23775 |
. . . 4
⊢ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
∈ (𝑈Homeo(MetOpen‘(ℝn‘1o)))
∧ 𝑌 ⊆ ℝ) → (𝑌 ∈ (Clsd‘𝑈) ↔ ((𝑥
∈ ℝ ↦ ({∅} × {𝑥}))
“ 𝑌) ∈
(Clsd‘(MetOpen‘(ℝn‘1o))))) |
| 78 | 73, 34, 77 | sylancr 587 |
. . 3
⊢ (𝑌 ⊆ ℝ → (𝑌 ∈ (Clsd‘𝑈) ↔ ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) ∈
(Clsd‘(MetOpen‘(ℝn‘1o))))) |
| 79 | | ismtybnd 37814 |
. . . 4
⊢ ((𝑀 ∈ (∞Met‘𝑌) ∧
((ℝn‘1o) ↾ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌))) ∈
(∞Met‘((𝑥
∈ ℝ ↦ ({∅} × {𝑥})) “ 𝑌)) ∧ ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) ↾ 𝑌) ∈ (𝑀 Ismty
((ℝn‘1o) ↾ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌))))) → (𝑀 ∈ (Bnd‘𝑌) ↔
((ℝn‘1o) ↾ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌))) ∈ (Bnd‘((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌)))) |
| 80 | 39, 41, 57, 79 | syl3anc 1373 |
. . 3
⊢ (𝑌 ⊆ ℝ → (𝑀 ∈ (Bnd‘𝑌) ↔
((ℝn‘1o) ↾ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) × ((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌))) ∈ (Bnd‘((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌)))) |
| 81 | 78, 80 | anbi12d 632 |
. 2
⊢ (𝑌 ⊆ ℝ → ((𝑌 ∈ (Clsd‘𝑈) ∧ 𝑀 ∈ (Bnd‘𝑌)) ↔ (((𝑥 ∈ ℝ ↦ ({∅} ×
{𝑥})) “ 𝑌) ∈
(Clsd‘(MetOpen‘(ℝn‘1o)))
∧ ((ℝn‘1o) ↾ (((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌) × ((𝑥 ∈ ℝ ↦
({∅} × {𝑥}))
“ 𝑌))) ∈
(Bnd‘((𝑥 ∈
ℝ ↦ ({∅} × {𝑥})) “ 𝑌))))) |
| 82 | 31, 66, 81 | 3bitr4d 311 |
1
⊢ (𝑌 ⊆ ℝ → (𝑇 ∈ Comp ↔ (𝑌 ∈ (Clsd‘𝑈) ∧ 𝑀 ∈ (Bnd‘𝑌)))) |