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 ⊢ 𝑀 = ( ( abs ∘ − ) ↾ ( 𝑌 × 𝑌 ) )
reheibor.3 ⊢ 𝑇 = ( MetOpen ‘ 𝑀 )
reheibor.4 ⊢ 𝑈 = ( topGen ‘ ran (,) )
Assertion reheibor ( 𝑌 ⊆ ℝ → ( 𝑇 ∈ Comp ↔ ( 𝑌 ∈ ( Clsd ‘ 𝑈 ) ∧ 𝑀 ∈ ( Bnd ‘ 𝑌 ) ) ) )

Proof

Step Hyp Ref Expression
1 reheibor.2 ⊢ 𝑀 = ( ( abs ∘ − ) ↾ ( 𝑌 × 𝑌 ) )
2 reheibor.3 ⊢ 𝑇 = ( MetOpen ‘ 𝑀 )
3 reheibor.4 ⊢ 𝑈 = ( topGen ‘ ran (,) )
4 df1o2 ⊢ 1o = { ∅ }
5 snfi ⊢ { ∅ } ∈ Fin
6 4 5 eqeltri ⊢ 1o ∈ Fin
7 imassrn ⊢ ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ⊆ ran ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) )
8 0ex ⊢ ∅ ∈ V
9 eqid ⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
10 eqid ⊢ ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) = ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) )
11 9 10 ismrer1 ⊢ ( ∅ ∈ V → ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) ∈ ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) Ismty ( ℝn ‘ { ∅ } ) ) )
12 8 11 ax-mp ⊢ ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) ∈ ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) Ismty ( ℝn ‘ { ∅ } ) )
13 4 fveq2i ⊢ ( ℝn ‘ 1o ) = ( ℝn ‘ { ∅ } )
14 13 oveq2i ⊢ ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) Ismty ( ℝn ‘ 1o ) ) = ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) Ismty ( ℝn ‘ { ∅ } ) )
15 12 14 eleqtrri ⊢ ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) ∈ ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) Ismty ( ℝn ‘ 1o ) )
16 9 rexmet ⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ )
17 eqid ⊢ ( ℝ ↑m 1o ) = ( ℝ ↑m 1o )
18 17 rrnmet ⊢ ( 1o ∈ Fin → ( ℝn ‘ 1o ) ∈ ( Met ‘ ( ℝ ↑m 1o ) ) )
19 metxmet ⊢ ( ( ℝn ‘ 1o ) ∈ ( Met ‘ ( ℝ ↑m 1o ) ) → ( ℝn ‘ 1o ) ∈ ( ∞Met ‘ ( ℝ ↑m 1o ) ) )
20 6 18 19 mp2b ⊢ ( ℝn ‘ 1o ) ∈ ( ∞Met ‘ ( ℝ ↑m 1o ) )
21 isismty ⊢ ( ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ ) ∧ ( ℝn ‘ 1o ) ∈ ( ∞Met ‘ ( ℝ ↑m 1o ) ) ) → ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) ∈ ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) Ismty ( ℝn ‘ 1o ) ) ↔ ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) : ℝ –1-1-onto→ ( ℝ ↑m 1o ) ∧ ∀ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ℝ ( 𝑦 ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) 𝑧 ) = ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) ‘ 𝑦 ) ( ℝn ‘ 1o ) ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) ‘ 𝑧 ) ) ) ) )
22 16 20 21 mp2an ⊢ ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) ∈ ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) Ismty ( ℝn ‘ 1o ) ) ↔ ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) : ℝ –1-1-onto→ ( ℝ ↑m 1o ) ∧ ∀ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ℝ ( 𝑦 ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) 𝑧 ) = ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) ‘ 𝑦 ) ( ℝn ‘ 1o ) ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) ‘ 𝑧 ) ) ) )
23 15 22 mpbi ⊢ ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) : ℝ –1-1-onto→ ( ℝ ↑m 1o ) ∧ ∀ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ℝ ( 𝑦 ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) 𝑧 ) = ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) ‘ 𝑦 ) ( ℝn ‘ 1o ) ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) ‘ 𝑧 ) ) )
24 23 simpli ⊢ ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) : ℝ –1-1-onto→ ( ℝ ↑m 1o )
25 f1of ⊢ ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) : ℝ –1-1-onto→ ( ℝ ↑m 1o ) → ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) : ℝ ⟶ ( ℝ ↑m 1o ) )
26 frn ⊢ ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) : ℝ ⟶ ( ℝ ↑m 1o ) → ran ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) ⊆ ( ℝ ↑m 1o ) )
27 24 25 26 mp2b ⊢ ran ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) ⊆ ( ℝ ↑m 1o )
28 7 27 sstri ⊢ ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ⊆ ( ℝ ↑m 1o )
29 28 a1i ⊢ ( 𝑌 ⊆ ℝ → ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ⊆ ( ℝ ↑m 1o ) )
30 eqid ⊢ ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) = ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) )
31 eqid ⊢ ( MetOpen ‘ ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ) = ( MetOpen ‘ ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) )
32 eqid ⊢ ( MetOpen ‘ ( ℝn ‘ 1o ) ) = ( MetOpen ‘ ( ℝn ‘ 1o ) )
33 17 30 31 32 rrnheibor ⊢ ( ( 1o ∈ Fin ∧ ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ⊆ ( ℝ ↑m 1o ) ) → ( ( MetOpen ‘ ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ) ∈ Comp ↔ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ∈ ( Clsd ‘ ( MetOpen ‘ ( ℝn ‘ 1o ) ) ) ∧ ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ∈ ( Bnd ‘ ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ) )
34 6 29 33 sylancr ⊢ ( 𝑌 ⊆ ℝ → ( ( MetOpen ‘ ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ) ∈ Comp ↔ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ∈ ( Clsd ‘ ( MetOpen ‘ ( ℝn ‘ 1o ) ) ) ∧ ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ∈ ( Bnd ‘ ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ) )
35 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
36 id ⊢ ( 𝑌 ⊆ ℝ → 𝑌 ⊆ ℝ )
37 ax-resscn ⊢ ℝ ⊆ ℂ
38 36 37 sstrdi ⊢ ( 𝑌 ⊆ ℝ → 𝑌 ⊆ ℂ )
39 xmetres2 ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑌 ⊆ ℂ ) → ( ( abs ∘ − ) ↾ ( 𝑌 × 𝑌 ) ) ∈ ( ∞Met ‘ 𝑌 ) )
40 35 38 39 sylancr ⊢ ( 𝑌 ⊆ ℝ → ( ( abs ∘ − ) ↾ ( 𝑌 × 𝑌 ) ) ∈ ( ∞Met ‘ 𝑌 ) )
41 1 40 eqeltrid ⊢ ( 𝑌 ⊆ ℝ → 𝑀 ∈ ( ∞Met ‘ 𝑌 ) )
42 xmetres2 ⊢ ( ( ( ℝn ‘ 1o ) ∈ ( ∞Met ‘ ( ℝ ↑m 1o ) ) ∧ ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ⊆ ( ℝ ↑m 1o ) ) → ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ∈ ( ∞Met ‘ ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) )
43 20 29 42 sylancr ⊢ ( 𝑌 ⊆ ℝ → ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ∈ ( ∞Met ‘ ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) )
44 2 31 ismtyhmeo ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑌 ) ∧ ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ∈ ( ∞Met ‘ ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) → ( 𝑀 Ismty ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ) ⊆ ( 𝑇 Homeo ( MetOpen ‘ ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ) ) )
45 41 43 44 syl2anc ⊢ ( 𝑌 ⊆ ℝ → ( 𝑀 Ismty ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ) ⊆ ( 𝑇 Homeo ( MetOpen ‘ ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ) ) )
46 16 a1i ⊢ ( 𝑌 ⊆ ℝ → ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ ) )
47 20 a1i ⊢ ( 𝑌 ⊆ ℝ → ( ℝn ‘ 1o ) ∈ ( ∞Met ‘ ( ℝ ↑m 1o ) ) )
48 15 a1i ⊢ ( 𝑌 ⊆ ℝ → ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) ∈ ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) Ismty ( ℝn ‘ 1o ) ) )
49 eqid ⊢ ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) = ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 )
50 eqid ⊢ ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ↾ ( 𝑌 × 𝑌 ) ) = ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ↾ ( 𝑌 × 𝑌 ) )
51 49 50 30 ismtyres ⊢ ( ( ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ ) ∧ ( ℝn ‘ 1o ) ∈ ( ∞Met ‘ ( ℝ ↑m 1o ) ) ) ∧ ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) ∈ ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) Ismty ( ℝn ‘ 1o ) ) ∧ 𝑌 ⊆ ℝ ) ) → ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) ↾ 𝑌 ) ∈ ( ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ↾ ( 𝑌 × 𝑌 ) ) Ismty ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ) )
52 46 47 48 36 51 syl22anc ⊢ ( 𝑌 ⊆ ℝ → ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) ↾ 𝑌 ) ∈ ( ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ↾ ( 𝑌 × 𝑌 ) ) Ismty ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ) )
53 xpss12 ⊢ ( ( 𝑌 ⊆ ℝ ∧ 𝑌 ⊆ ℝ ) → ( 𝑌 × 𝑌 ) ⊆ ( ℝ × ℝ ) )
54 53 anidms ⊢ ( 𝑌 ⊆ ℝ → ( 𝑌 × 𝑌 ) ⊆ ( ℝ × ℝ ) )
55 54 resabs1d ⊢ ( 𝑌 ⊆ ℝ → ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ↾ ( 𝑌 × 𝑌 ) ) = ( ( abs ∘ − ) ↾ ( 𝑌 × 𝑌 ) ) )
56 55 1 eqtr4di ⊢ ( 𝑌 ⊆ ℝ → ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ↾ ( 𝑌 × 𝑌 ) ) = 𝑀 )
57 56 oveq1d ⊢ ( 𝑌 ⊆ ℝ → ( ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ↾ ( 𝑌 × 𝑌 ) ) Ismty ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ) = ( 𝑀 Ismty ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ) )
58 52 57 eleqtrd ⊢ ( 𝑌 ⊆ ℝ → ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) ↾ 𝑌 ) ∈ ( 𝑀 Ismty ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ) )
59 45 58 sseldd ⊢ ( 𝑌 ⊆ ℝ → ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) ↾ 𝑌 ) ∈ ( 𝑇 Homeo ( MetOpen ‘ ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ) ) )
60 hmphi ⊢ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) ↾ 𝑌 ) ∈ ( 𝑇 Homeo ( MetOpen ‘ ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ) ) → 𝑇 ≃ ( MetOpen ‘ ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ) )
61 59 60 syl ⊢ ( 𝑌 ⊆ ℝ → 𝑇 ≃ ( MetOpen ‘ ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ) )
62 cmphmph ⊢ ( 𝑇 ≃ ( MetOpen ‘ ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ) → ( 𝑇 ∈ Comp → ( MetOpen ‘ ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ) ∈ Comp ) )
63 hmphsym ⊢ ( 𝑇 ≃ ( MetOpen ‘ ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ) → ( MetOpen ‘ ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ) ≃ 𝑇 )
64 cmphmph ⊢ ( ( MetOpen ‘ ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ) ≃ 𝑇 → ( ( MetOpen ‘ ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ) ∈ Comp → 𝑇 ∈ Comp ) )
65 63 64 syl ⊢ ( 𝑇 ≃ ( MetOpen ‘ ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ) → ( ( MetOpen ‘ ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ) ∈ Comp → 𝑇 ∈ Comp ) )
66 62 65 impbid ⊢ ( 𝑇 ≃ ( MetOpen ‘ ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ) → ( 𝑇 ∈ Comp ↔ ( MetOpen ‘ ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ) ∈ Comp ) )
67 61 66 syl ⊢ ( 𝑌 ⊆ ℝ → ( 𝑇 ∈ Comp ↔ ( MetOpen ‘ ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ) ∈ Comp ) )
68 eqid ⊢ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
69 9 68 tgioo ⊢ ( topGen ‘ ran (,) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
70 3 69 eqtri ⊢ 𝑈 = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
71 70 32 ismtyhmeo ⊢ ( ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ ) ∧ ( ℝn ‘ 1o ) ∈ ( ∞Met ‘ ( ℝ ↑m 1o ) ) ) → ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) Ismty ( ℝn ‘ 1o ) ) ⊆ ( 𝑈 Homeo ( MetOpen ‘ ( ℝn ‘ 1o ) ) ) )
72 16 20 71 mp2an ⊢ ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) Ismty ( ℝn ‘ 1o ) ) ⊆ ( 𝑈 Homeo ( MetOpen ‘ ( ℝn ‘ 1o ) ) )
73 72 15 sselii ⊢ ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) ∈ ( 𝑈 Homeo ( MetOpen ‘ ( ℝn ‘ 1o ) ) )
74 retopon ⊢ ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ )
75 3 74 eqeltri ⊢ 𝑈 ∈ ( TopOn ‘ ℝ )
76 75 toponunii ⊢ ℝ = ∪ 𝑈
77 76 hmeocld ⊢ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) ∈ ( 𝑈 Homeo ( MetOpen ‘ ( ℝn ‘ 1o ) ) ) ∧ 𝑌 ⊆ ℝ ) → ( 𝑌 ∈ ( Clsd ‘ 𝑈 ) ↔ ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ∈ ( Clsd ‘ ( MetOpen ‘ ( ℝn ‘ 1o ) ) ) ) )
78 73 36 77 sylancr ⊢ ( 𝑌 ⊆ ℝ → ( 𝑌 ∈ ( Clsd ‘ 𝑈 ) ↔ ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ∈ ( Clsd ‘ ( MetOpen ‘ ( ℝn ‘ 1o ) ) ) ) )
79 ismtybnd ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑌 ) ∧ ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ∈ ( ∞Met ‘ ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ∧ ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) ↾ 𝑌 ) ∈ ( 𝑀 Ismty ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ) ) → ( 𝑀 ∈ ( Bnd ‘ 𝑌 ) ↔ ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ∈ ( Bnd ‘ ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) )
80 41 43 58 79 syl3anc ⊢ ( 𝑌 ⊆ ℝ → ( 𝑀 ∈ ( Bnd ‘ 𝑌 ) ↔ ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ∈ ( Bnd ‘ ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) )
81 78 80 anbi12d ⊢ ( 𝑌 ⊆ ℝ → ( ( 𝑌 ∈ ( Clsd ‘ 𝑈 ) ∧ 𝑀 ∈ ( Bnd ‘ 𝑌 ) ) ↔ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ∈ ( Clsd ‘ ( MetOpen ‘ ( ℝn ‘ 1o ) ) ) ∧ ( ( ℝn ‘ 1o ) ↾ ( ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) × ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ∈ ( Bnd ‘ ( ( 𝑥 ∈ ℝ ↦ ( { ∅ } × { 𝑥 } ) ) “ 𝑌 ) ) ) ) )
82 34 67 81 3bitr4d ⊢ ( 𝑌 ⊆ ℝ → ( 𝑇 ∈ Comp ↔ ( 𝑌 ∈ ( Clsd ‘ 𝑈 ) ∧ 𝑀 ∈ ( Bnd ‘ 𝑌 ) ) ) )