# Metamath Proof Explorer

## Theorem reheibor

Description: Heine-Borel theorem for real numbers. A subset of RR is compact iff it is closed and bounded. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 22-Sep-2015)

Ref Expression
Hypotheses reheibor.2 ${⊢}{M}={\left(\mathrm{abs}\circ -\right)↾}_{\left({Y}×{Y}\right)}$
reheibor.3 ${⊢}{T}=\mathrm{MetOpen}\left({M}\right)$
reheibor.4 ${⊢}{U}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
Assertion reheibor ${⊢}{Y}\subseteq ℝ\to \left({T}\in \mathrm{Comp}↔\left({Y}\in \mathrm{Clsd}\left({U}\right)\wedge {M}\in \mathrm{Bnd}\left({Y}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 reheibor.2 ${⊢}{M}={\left(\mathrm{abs}\circ -\right)↾}_{\left({Y}×{Y}\right)}$
2 reheibor.3 ${⊢}{T}=\mathrm{MetOpen}\left({M}\right)$
3 reheibor.4 ${⊢}{U}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
4 df1o2 ${⊢}{1}_{𝑜}=\left\{\varnothing \right\}$
5 snfi ${⊢}\left\{\varnothing \right\}\in \mathrm{Fin}$
6 4 5 eqeltri ${⊢}{1}_{𝑜}\in \mathrm{Fin}$
7 imassrn ${⊢}\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\subseteq \mathrm{ran}\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)$
8 0ex ${⊢}\varnothing \in \mathrm{V}$
9 eqid ${⊢}{\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}={\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}$
10 eqid ${⊢}\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)=\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)$
11 9 10 ismrer1 ${⊢}\varnothing \in \mathrm{V}\to \left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\in \left(\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right)\mathrm{Ismty}{ℝ}^{n}\left(\left\{\varnothing \right\}\right)\right)$
12 8 11 ax-mp ${⊢}\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\in \left(\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right)\mathrm{Ismty}{ℝ}^{n}\left(\left\{\varnothing \right\}\right)\right)$
13 4 fveq2i ${⊢}{ℝ}^{n}\left({1}_{𝑜}\right)={ℝ}^{n}\left(\left\{\varnothing \right\}\right)$
14 13 oveq2i ${⊢}\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right)\mathrm{Ismty}{ℝ}^{n}\left({1}_{𝑜}\right)=\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right)\mathrm{Ismty}{ℝ}^{n}\left(\left\{\varnothing \right\}\right)$
15 12 14 eleqtrri ${⊢}\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\in \left(\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right)\mathrm{Ismty}{ℝ}^{n}\left({1}_{𝑜}\right)\right)$
16 9 rexmet ${⊢}{\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\in \mathrm{\infty Met}\left(ℝ\right)$
17 eqid ${⊢}{ℝ}^{{1}_{𝑜}}={ℝ}^{{1}_{𝑜}}$
18 17 rrnmet ${⊢}{1}_{𝑜}\in \mathrm{Fin}\to {ℝ}^{n}\left({1}_{𝑜}\right)\in \mathrm{Met}\left({ℝ}^{{1}_{𝑜}}\right)$
19 metxmet ${⊢}{ℝ}^{n}\left({1}_{𝑜}\right)\in \mathrm{Met}\left({ℝ}^{{1}_{𝑜}}\right)\to {ℝ}^{n}\left({1}_{𝑜}\right)\in \mathrm{\infty Met}\left({ℝ}^{{1}_{𝑜}}\right)$
20 6 18 19 mp2b ${⊢}{ℝ}^{n}\left({1}_{𝑜}\right)\in \mathrm{\infty Met}\left({ℝ}^{{1}_{𝑜}}\right)$
21 isismty ${⊢}\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\in \mathrm{\infty Met}\left(ℝ\right)\wedge {ℝ}^{n}\left({1}_{𝑜}\right)\in \mathrm{\infty Met}\left({ℝ}^{{1}_{𝑜}}\right)\right)\to \left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\in \left(\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right)\mathrm{Ismty}{ℝ}^{n}\left({1}_{𝑜}\right)\right)↔\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right):ℝ\underset{1-1 onto}{⟶}{ℝ}^{{1}_{𝑜}}\wedge \forall {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}{y}\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right){z}=\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left({y}\right){ℝ}^{n}\left({1}_{𝑜}\right)\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left({z}\right)\right)\right)$
22 16 20 21 mp2an ${⊢}\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\in \left(\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right)\mathrm{Ismty}{ℝ}^{n}\left({1}_{𝑜}\right)\right)↔\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right):ℝ\underset{1-1 onto}{⟶}{ℝ}^{{1}_{𝑜}}\wedge \forall {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}{y}\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right){z}=\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left({y}\right){ℝ}^{n}\left({1}_{𝑜}\right)\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left({z}\right)\right)$
23 15 22 mpbi ${⊢}\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right):ℝ\underset{1-1 onto}{⟶}{ℝ}^{{1}_{𝑜}}\wedge \forall {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}{y}\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right){z}=\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left({y}\right){ℝ}^{n}\left({1}_{𝑜}\right)\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left({z}\right)\right)$
24 23 simpli ${⊢}\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right):ℝ\underset{1-1 onto}{⟶}{ℝ}^{{1}_{𝑜}}$
25 f1of ${⊢}\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right):ℝ\underset{1-1 onto}{⟶}{ℝ}^{{1}_{𝑜}}\to \left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right):ℝ⟶{ℝ}^{{1}_{𝑜}}$
26 frn ${⊢}\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right):ℝ⟶{ℝ}^{{1}_{𝑜}}\to \mathrm{ran}\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\subseteq {ℝ}^{{1}_{𝑜}}$
27 24 25 26 mp2b ${⊢}\mathrm{ran}\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\subseteq {ℝ}^{{1}_{𝑜}}$
28 7 27 sstri ${⊢}\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\subseteq {ℝ}^{{1}_{𝑜}}$
29 28 a1i ${⊢}{Y}\subseteq ℝ\to \left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\subseteq {ℝ}^{{1}_{𝑜}}$
30 eqid ${⊢}{{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}={{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}$
31 eqid ${⊢}\mathrm{MetOpen}\left({{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\right)=\mathrm{MetOpen}\left({{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\right)$
32 eqid ${⊢}\mathrm{MetOpen}\left({ℝ}^{n}\left({1}_{𝑜}\right)\right)=\mathrm{MetOpen}\left({ℝ}^{n}\left({1}_{𝑜}\right)\right)$
33 17 30 31 32 rrnheibor ${⊢}\left({1}_{𝑜}\in \mathrm{Fin}\wedge \left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\subseteq {ℝ}^{{1}_{𝑜}}\right)\to \left(\mathrm{MetOpen}\left({{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\right)\in \mathrm{Comp}↔\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\in \mathrm{Clsd}\left(\mathrm{MetOpen}\left({ℝ}^{n}\left({1}_{𝑜}\right)\right)\right)\wedge {{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\in \mathrm{Bnd}\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)\right)\right)$
34 6 29 33 sylancr ${⊢}{Y}\subseteq ℝ\to \left(\mathrm{MetOpen}\left({{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\right)\in \mathrm{Comp}↔\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\in \mathrm{Clsd}\left(\mathrm{MetOpen}\left({ℝ}^{n}\left({1}_{𝑜}\right)\right)\right)\wedge {{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\in \mathrm{Bnd}\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)\right)\right)$
35 cnxmet ${⊢}\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)$
36 id ${⊢}{Y}\subseteq ℝ\to {Y}\subseteq ℝ$
37 ax-resscn ${⊢}ℝ\subseteq ℂ$
38 36 37 sstrdi ${⊢}{Y}\subseteq ℝ\to {Y}\subseteq ℂ$
39 xmetres2 ${⊢}\left(\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)\wedge {Y}\subseteq ℂ\right)\to {\left(\mathrm{abs}\circ -\right)↾}_{\left({Y}×{Y}\right)}\in \mathrm{\infty Met}\left({Y}\right)$
40 35 38 39 sylancr ${⊢}{Y}\subseteq ℝ\to {\left(\mathrm{abs}\circ -\right)↾}_{\left({Y}×{Y}\right)}\in \mathrm{\infty Met}\left({Y}\right)$
41 1 40 eqeltrid ${⊢}{Y}\subseteq ℝ\to {M}\in \mathrm{\infty Met}\left({Y}\right)$
42 xmetres2 ${⊢}\left({ℝ}^{n}\left({1}_{𝑜}\right)\in \mathrm{\infty Met}\left({ℝ}^{{1}_{𝑜}}\right)\wedge \left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\subseteq {ℝ}^{{1}_{𝑜}}\right)\to {{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\in \mathrm{\infty Met}\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)$
43 20 29 42 sylancr ${⊢}{Y}\subseteq ℝ\to {{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\in \mathrm{\infty Met}\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)$
44 2 31 ismtyhmeo ${⊢}\left({M}\in \mathrm{\infty Met}\left({Y}\right)\wedge {{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\in \mathrm{\infty Met}\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)\right)\to {M}\mathrm{Ismty}\left({{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\right)\subseteq {T}\mathrm{Homeo}\mathrm{MetOpen}\left({{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\right)$
45 41 43 44 syl2anc ${⊢}{Y}\subseteq ℝ\to {M}\mathrm{Ismty}\left({{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\right)\subseteq {T}\mathrm{Homeo}\mathrm{MetOpen}\left({{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\right)$
46 16 a1i ${⊢}{Y}\subseteq ℝ\to {\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\in \mathrm{\infty Met}\left(ℝ\right)$
47 20 a1i ${⊢}{Y}\subseteq ℝ\to {ℝ}^{n}\left({1}_{𝑜}\right)\in \mathrm{\infty Met}\left({ℝ}^{{1}_{𝑜}}\right)$
48 15 a1i ${⊢}{Y}\subseteq ℝ\to \left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\in \left(\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right)\mathrm{Ismty}{ℝ}^{n}\left({1}_{𝑜}\right)\right)$
49 eqid ${⊢}\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]=\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]$
50 eqid ${⊢}{\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right)↾}_{\left({Y}×{Y}\right)}={\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right)↾}_{\left({Y}×{Y}\right)}$
51 49 50 30 ismtyres ${⊢}\left(\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\in \mathrm{\infty Met}\left(ℝ\right)\wedge {ℝ}^{n}\left({1}_{𝑜}\right)\in \mathrm{\infty Met}\left({ℝ}^{{1}_{𝑜}}\right)\right)\wedge \left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\in \left(\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right)\mathrm{Ismty}{ℝ}^{n}\left({1}_{𝑜}\right)\right)\wedge {Y}\subseteq ℝ\right)\right)\to {\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)↾}_{{Y}}\in \left(\left({\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right)↾}_{\left({Y}×{Y}\right)}\right)\mathrm{Ismty}\left({{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\right)\right)$
52 46 47 48 36 51 syl22anc ${⊢}{Y}\subseteq ℝ\to {\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)↾}_{{Y}}\in \left(\left({\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right)↾}_{\left({Y}×{Y}\right)}\right)\mathrm{Ismty}\left({{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\right)\right)$
53 xpss12 ${⊢}\left({Y}\subseteq ℝ\wedge {Y}\subseteq ℝ\right)\to {Y}×{Y}\subseteq {ℝ}^{2}$
54 53 anidms ${⊢}{Y}\subseteq ℝ\to {Y}×{Y}\subseteq {ℝ}^{2}$
55 54 resabs1d ${⊢}{Y}\subseteq ℝ\to {\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right)↾}_{\left({Y}×{Y}\right)}={\left(\mathrm{abs}\circ -\right)↾}_{\left({Y}×{Y}\right)}$
56 55 1 eqtr4di ${⊢}{Y}\subseteq ℝ\to {\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right)↾}_{\left({Y}×{Y}\right)}={M}$
57 56 oveq1d ${⊢}{Y}\subseteq ℝ\to \left({\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right)↾}_{\left({Y}×{Y}\right)}\right)\mathrm{Ismty}\left({{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\right)={M}\mathrm{Ismty}\left({{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\right)$
58 52 57 eleqtrd ${⊢}{Y}\subseteq ℝ\to {\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)↾}_{{Y}}\in \left({M}\mathrm{Ismty}\left({{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\right)\right)$
59 45 58 sseldd ${⊢}{Y}\subseteq ℝ\to {\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)↾}_{{Y}}\in \left({T}\mathrm{Homeo}\mathrm{MetOpen}\left({{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\right)\right)$
60 hmphi ${⊢}{\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)↾}_{{Y}}\in \left({T}\mathrm{Homeo}\mathrm{MetOpen}\left({{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\right)\right)\to {T}\simeq \mathrm{MetOpen}\left({{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\right)$
61 59 60 syl ${⊢}{Y}\subseteq ℝ\to {T}\simeq \mathrm{MetOpen}\left({{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\right)$
62 cmphmph ${⊢}{T}\simeq \mathrm{MetOpen}\left({{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\right)\to \left({T}\in \mathrm{Comp}\to \mathrm{MetOpen}\left({{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\right)\in \mathrm{Comp}\right)$
63 hmphsym ${⊢}{T}\simeq \mathrm{MetOpen}\left({{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\right)\to \mathrm{MetOpen}\left({{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\right)\simeq {T}$
64 cmphmph ${⊢}\mathrm{MetOpen}\left({{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\right)\simeq {T}\to \left(\mathrm{MetOpen}\left({{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\right)\in \mathrm{Comp}\to {T}\in \mathrm{Comp}\right)$
65 63 64 syl ${⊢}{T}\simeq \mathrm{MetOpen}\left({{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\right)\to \left(\mathrm{MetOpen}\left({{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\right)\in \mathrm{Comp}\to {T}\in \mathrm{Comp}\right)$
66 62 65 impbid ${⊢}{T}\simeq \mathrm{MetOpen}\left({{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\right)\to \left({T}\in \mathrm{Comp}↔\mathrm{MetOpen}\left({{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\right)\in \mathrm{Comp}\right)$
67 61 66 syl ${⊢}{Y}\subseteq ℝ\to \left({T}\in \mathrm{Comp}↔\mathrm{MetOpen}\left({{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\right)\in \mathrm{Comp}\right)$
68 eqid ${⊢}\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right)=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right)$
69 9 68 tgioo ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right)$
70 3 69 eqtri ${⊢}{U}=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right)$
71 70 32 ismtyhmeo ${⊢}\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\in \mathrm{\infty Met}\left(ℝ\right)\wedge {ℝ}^{n}\left({1}_{𝑜}\right)\in \mathrm{\infty Met}\left({ℝ}^{{1}_{𝑜}}\right)\right)\to \left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right)\mathrm{Ismty}{ℝ}^{n}\left({1}_{𝑜}\right)\subseteq {U}\mathrm{Homeo}\mathrm{MetOpen}\left({ℝ}^{n}\left({1}_{𝑜}\right)\right)$
72 16 20 71 mp2an ${⊢}\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right)\mathrm{Ismty}{ℝ}^{n}\left({1}_{𝑜}\right)\subseteq {U}\mathrm{Homeo}\mathrm{MetOpen}\left({ℝ}^{n}\left({1}_{𝑜}\right)\right)$
73 72 15 sselii ${⊢}\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\in \left({U}\mathrm{Homeo}\mathrm{MetOpen}\left({ℝ}^{n}\left({1}_{𝑜}\right)\right)\right)$
74 retopon ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{TopOn}\left(ℝ\right)$
75 3 74 eqeltri ${⊢}{U}\in \mathrm{TopOn}\left(ℝ\right)$
76 75 toponunii ${⊢}ℝ=\bigcup {U}$
77 76 hmeocld ${⊢}\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\in \left({U}\mathrm{Homeo}\mathrm{MetOpen}\left({ℝ}^{n}\left({1}_{𝑜}\right)\right)\right)\wedge {Y}\subseteq ℝ\right)\to \left({Y}\in \mathrm{Clsd}\left({U}\right)↔\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\in \mathrm{Clsd}\left(\mathrm{MetOpen}\left({ℝ}^{n}\left({1}_{𝑜}\right)\right)\right)\right)$
78 73 36 77 sylancr ${⊢}{Y}\subseteq ℝ\to \left({Y}\in \mathrm{Clsd}\left({U}\right)↔\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\in \mathrm{Clsd}\left(\mathrm{MetOpen}\left({ℝ}^{n}\left({1}_{𝑜}\right)\right)\right)\right)$
79 ismtybnd ${⊢}\left({M}\in \mathrm{\infty Met}\left({Y}\right)\wedge {{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\in \mathrm{\infty Met}\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)\wedge {\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)↾}_{{Y}}\in \left({M}\mathrm{Ismty}\left({{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\right)\right)\right)\to \left({M}\in \mathrm{Bnd}\left({Y}\right)↔{{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\in \mathrm{Bnd}\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)\right)$
80 41 43 58 79 syl3anc ${⊢}{Y}\subseteq ℝ\to \left({M}\in \mathrm{Bnd}\left({Y}\right)↔{{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\in \mathrm{Bnd}\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)\right)$
81 78 80 anbi12d ${⊢}{Y}\subseteq ℝ\to \left(\left({Y}\in \mathrm{Clsd}\left({U}\right)\wedge {M}\in \mathrm{Bnd}\left({Y}\right)\right)↔\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\in \mathrm{Clsd}\left(\mathrm{MetOpen}\left({ℝ}^{n}\left({1}_{𝑜}\right)\right)\right)\wedge {{ℝ}^{n}\left({1}_{𝑜}\right)↾}_{\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]×\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)}\in \mathrm{Bnd}\left(\left({x}\in ℝ⟼\left\{\varnothing \right\}×\left\{{x}\right\}\right)\left[{Y}\right]\right)\right)\right)$
82 34 67 81 3bitr4d ${⊢}{Y}\subseteq ℝ\to \left({T}\in \mathrm{Comp}↔\left({Y}\in \mathrm{Clsd}\left({U}\right)\wedge {M}\in \mathrm{Bnd}\left({Y}\right)\right)\right)$