Metamath Proof Explorer

Theorem xrsmopn

Description: The metric on the extended reals generates a topology, but this does not match the order topology on RR* ; for example { +oo } is open in the metric topology, but not the order topology. However, the metric topology is finer than the order topology, meaning that all open intervals are open in the metric topology. (Contributed by Mario Carneiro, 4-Sep-2015)

Ref Expression
Hypotheses xrsxmet.1 ⊢ 𝐷 = ( dist ‘ ℝ*𝑠 )
xrsmopn.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion xrsmopn ( ordTop ‘ ≤ ) ⊆ 𝐽

Proof

Step Hyp Ref Expression
1 xrsxmet.1 ⊢ 𝐷 = ( dist ‘ ℝ*𝑠 )
2 xrsmopn.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
3 elssuni ⊢ ( 𝑥 ∈ ( ordTop ‘ ≤ ) → 𝑥 ⊆ ∪ ( ordTop ‘ ≤ ) )
4 letopuni ⊢ ℝ* = ∪ ( ordTop ‘ ≤ )
5 3 4 sseqtrrdi ⊢ ( 𝑥 ∈ ( ordTop ‘ ≤ ) → 𝑥 ⊆ ℝ* )
6 eqid ⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
7 6 rexmet ⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ )
8 letop ⊢ ( ordTop ‘ ≤ ) ∈ Top
9 reex ⊢ ℝ ∈ V
10 elrestr ⊢ ( ( ( ordTop ‘ ≤ ) ∈ Top ∧ ℝ ∈ V ∧ 𝑥 ∈ ( ordTop ‘ ≤ ) ) → ( 𝑥 ∩ ℝ ) ∈ ( ( ordTop ‘ ≤ ) ↾t ℝ ) )
11 8 9 10 mp3an12 ⊢ ( 𝑥 ∈ ( ordTop ‘ ≤ ) → ( 𝑥 ∩ ℝ ) ∈ ( ( ordTop ‘ ≤ ) ↾t ℝ ) )
12 11 ad2antrr ⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑦 ∈ ℝ ) → ( 𝑥 ∩ ℝ ) ∈ ( ( ordTop ‘ ≤ ) ↾t ℝ ) )
13 elin ⊢ ( 𝑦 ∈ ( 𝑥 ∩ ℝ ) ↔ ( 𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ℝ ) )
14 13 biimpri ⊢ ( ( 𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ( 𝑥 ∩ ℝ ) )
15 14 adantll ⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ( 𝑥 ∩ ℝ ) )
16 eqid ⊢ ( ( ordTop ‘ ≤ ) ↾t ℝ ) = ( ( ordTop ‘ ≤ ) ↾t ℝ )
17 16 xrtgioo ⊢ ( topGen ‘ ran (,) ) = ( ( ordTop ‘ ≤ ) ↾t ℝ )
18 eqid ⊢ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
19 6 18 tgioo ⊢ ( topGen ‘ ran (,) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
20 17 19 eqtr3i ⊢ ( ( ordTop ‘ ≤ ) ↾t ℝ ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
21 20 mopni2 ⊢ ( ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ ) ∧ ( 𝑥 ∩ ℝ ) ∈ ( ( ordTop ‘ ≤ ) ↾t ℝ ) ∧ 𝑦 ∈ ( 𝑥 ∩ ℝ ) ) → ∃ 𝑟 ∈ ℝ+ ( 𝑦 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ ( 𝑥 ∩ ℝ ) )
22 7 12 15 21 mp3an2i ⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑦 ∈ ℝ ) → ∃ 𝑟 ∈ ℝ+ ( 𝑦 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ ( 𝑥 ∩ ℝ ) )
23 1 xrsxmet ⊢ 𝐷 ∈ ( ∞Met ‘ ℝ* )
24 simplr ⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) → 𝑦 ∈ ℝ )
25 ressxr ⊢ ℝ ⊆ ℝ*
26 sseqin2 ⊢ ( ℝ ⊆ ℝ* ↔ ( ℝ* ∩ ℝ ) = ℝ )
27 25 26 mpbi ⊢ ( ℝ* ∩ ℝ ) = ℝ
28 24 27 eleqtrrdi ⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) → 𝑦 ∈ ( ℝ* ∩ ℝ ) )
29 rpxr ⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ* )
30 29 adantl ⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) → 𝑟 ∈ ℝ* )
31 1 xrsdsre ⊢ ( 𝐷 ↾ ( ℝ × ℝ ) ) = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
32 31 eqcomi ⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) = ( 𝐷 ↾ ( ℝ × ℝ ) )
33 32 blres ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ ℝ* ) ∧ 𝑦 ∈ ( ℝ* ∩ ℝ ) ∧ 𝑟 ∈ ℝ* ) → ( 𝑦 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) = ( ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ∩ ℝ ) )
34 23 28 30 33 mp3an2i ⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝑦 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) = ( ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ∩ ℝ ) )
35 1 xrsblre ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑟 ∈ ℝ* ) → ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ℝ )
36 29 35 sylan2 ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑟 ∈ ℝ+ ) → ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ℝ )
37 36 adantll ⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ℝ )
38 dfss2 ⊢ ( ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ℝ ↔ ( ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ∩ ℝ ) = ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) )
39 37 38 sylib ⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) → ( ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ∩ ℝ ) = ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) )
40 34 39 eqtrd ⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝑦 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) = ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) )
41 40 sseq1d ⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) → ( ( 𝑦 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ ( 𝑥 ∩ ℝ ) ↔ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ( 𝑥 ∩ ℝ ) ) )
42 inss1 ⊢ ( 𝑥 ∩ ℝ ) ⊆ 𝑥
43 sstr ⊢ ( ( ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ( 𝑥 ∩ ℝ ) ∧ ( 𝑥 ∩ ℝ ) ⊆ 𝑥 ) → ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑥 )
44 42 43 mpan2 ⊢ ( ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ( 𝑥 ∩ ℝ ) → ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑥 )
45 41 44 biimtrdi ⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) → ( ( 𝑦 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ ( 𝑥 ∩ ℝ ) → ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑥 ) )
46 45 reximdva ⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑦 ∈ ℝ ) → ( ∃ 𝑟 ∈ ℝ+ ( 𝑦 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ ( 𝑥 ∩ ℝ ) → ∃ 𝑟 ∈ ℝ+ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑥 ) )
47 22 46 mpd ⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑦 ∈ ℝ ) → ∃ 𝑟 ∈ ℝ+ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑥 )
48 1rp ⊢ 1 ∈ ℝ+
49 5 sselda ⊢ ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ ℝ* )
50 49 adantr ⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ* )
51 rpxr ⊢ ( 1 ∈ ℝ+ → 1 ∈ ℝ* )
52 48 51 mp1i ⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ) → 1 ∈ ℝ* )
53 elbl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ ℝ* ) ∧ 𝑦 ∈ ℝ* ∧ 1 ∈ ℝ* ) → ( 𝑧 ∈ ( 𝑦 ( ball ‘ 𝐷 ) 1 ) ↔ ( 𝑧 ∈ ℝ* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) )
54 23 50 52 53 mp3an2i ⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ) → ( 𝑧 ∈ ( 𝑦 ( ball ‘ 𝐷 ) 1 ) ↔ ( 𝑧 ∈ ℝ* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) )
55 simp2 ⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) → ¬ 𝑦 ∈ ℝ )
56 49 3ad2ant1 ⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) → 𝑦 ∈ ℝ* )
57 56 adantr ⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) ∧ 𝑦 ≠ 𝑧 ) → 𝑦 ∈ ℝ* )
58 simpl3l ⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) ∧ 𝑦 ≠ 𝑧 ) → 𝑧 ∈ ℝ* )
59 xmetcl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ ℝ* ) ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) → ( 𝑦 𝐷 𝑧 ) ∈ ℝ* )
60 23 57 58 59 mp3an2i ⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) ∧ 𝑦 ≠ 𝑧 ) → ( 𝑦 𝐷 𝑧 ) ∈ ℝ* )
61 1red ⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) ∧ 𝑦 ≠ 𝑧 ) → 1 ∈ ℝ )
62 xmetge0 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ ℝ* ) ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) → 0 ≤ ( 𝑦 𝐷 𝑧 ) )
63 23 57 58 62 mp3an2i ⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) ∧ 𝑦 ≠ 𝑧 ) → 0 ≤ ( 𝑦 𝐷 𝑧 ) )
64 simpl3r ⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) ∧ 𝑦 ≠ 𝑧 ) → ( 𝑦 𝐷 𝑧 ) < 1 )
65 1xr ⊢ 1 ∈ ℝ*
66 xrltle ⊢ ( ( ( 𝑦 𝐷 𝑧 ) ∈ ℝ* ∧ 1 ∈ ℝ* ) → ( ( 𝑦 𝐷 𝑧 ) < 1 → ( 𝑦 𝐷 𝑧 ) ≤ 1 ) )
67 60 65 66 sylancl ⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) ∧ 𝑦 ≠ 𝑧 ) → ( ( 𝑦 𝐷 𝑧 ) < 1 → ( 𝑦 𝐷 𝑧 ) ≤ 1 ) )
68 64 67 mpd ⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) ∧ 𝑦 ≠ 𝑧 ) → ( 𝑦 𝐷 𝑧 ) ≤ 1 )
69 xrrege0 ⊢ ( ( ( ( 𝑦 𝐷 𝑧 ) ∈ ℝ* ∧ 1 ∈ ℝ ) ∧ ( 0 ≤ ( 𝑦 𝐷 𝑧 ) ∧ ( 𝑦 𝐷 𝑧 ) ≤ 1 ) ) → ( 𝑦 𝐷 𝑧 ) ∈ ℝ )
70 60 61 63 68 69 syl22anc ⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) ∧ 𝑦 ≠ 𝑧 ) → ( 𝑦 𝐷 𝑧 ) ∈ ℝ )
71 simpr ⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) ∧ 𝑦 ≠ 𝑧 ) → 𝑦 ≠ 𝑧 )
72 1 xrsdsreclb ⊢ ( ( 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ∧ 𝑦 ≠ 𝑧 ) → ( ( 𝑦 𝐷 𝑧 ) ∈ ℝ ↔ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) )
73 57 58 71 72 syl3anc ⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) ∧ 𝑦 ≠ 𝑧 ) → ( ( 𝑦 𝐷 𝑧 ) ∈ ℝ ↔ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) )
74 70 73 mpbid ⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) ∧ 𝑦 ≠ 𝑧 ) → ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) )
75 74 simpld ⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) ∧ 𝑦 ≠ 𝑧 ) → 𝑦 ∈ ℝ )
76 75 ex ⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) → ( 𝑦 ≠ 𝑧 → 𝑦 ∈ ℝ ) )
77 76 necon1bd ⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) → ( ¬ 𝑦 ∈ ℝ → 𝑦 = 𝑧 ) )
78 simp1r ⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) → 𝑦 ∈ 𝑥 )
79 elequ1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥 ) )
80 78 79 syl5ibcom ⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) → ( 𝑦 = 𝑧 → 𝑧 ∈ 𝑥 ) )
81 77 80 syld ⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) → ( ¬ 𝑦 ∈ ℝ → 𝑧 ∈ 𝑥 ) )
82 55 81 mpd ⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) → 𝑧 ∈ 𝑥 )
83 82 3expia ⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ) → ( ( 𝑧 ∈ ℝ* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) → 𝑧 ∈ 𝑥 ) )
84 54 83 sylbid ⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ) → ( 𝑧 ∈ ( 𝑦 ( ball ‘ 𝐷 ) 1 ) → 𝑧 ∈ 𝑥 ) )
85 84 ssrdv ⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ) → ( 𝑦 ( ball ‘ 𝐷 ) 1 ) ⊆ 𝑥 )
86 oveq2 ⊢ ( 𝑟 = 1 → ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) = ( 𝑦 ( ball ‘ 𝐷 ) 1 ) )
87 86 sseq1d ⊢ ( 𝑟 = 1 → ( ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑥 ↔ ( 𝑦 ( ball ‘ 𝐷 ) 1 ) ⊆ 𝑥 ) )
88 87 rspcev ⊢ ( ( 1 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ 𝐷 ) 1 ) ⊆ 𝑥 ) → ∃ 𝑟 ∈ ℝ+ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑥 )
89 48 85 88 sylancr ⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ) → ∃ 𝑟 ∈ ℝ+ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑥 )
90 47 89 pm2.61dan ⊢ ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑟 ∈ ℝ+ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑥 )
91 90 ralrimiva ⊢ ( 𝑥 ∈ ( ordTop ‘ ≤ ) → ∀ 𝑦 ∈ 𝑥 ∃ 𝑟 ∈ ℝ+ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑥 )
92 2 elmopn2 ⊢ ( 𝐷 ∈ ( ∞Met ‘ ℝ* ) → ( 𝑥 ∈ 𝐽 ↔ ( 𝑥 ⊆ ℝ* ∧ ∀ 𝑦 ∈ 𝑥 ∃ 𝑟 ∈ ℝ+ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑥 ) ) )
93 23 92 ax-mp ⊢ ( 𝑥 ∈ 𝐽 ↔ ( 𝑥 ⊆ ℝ* ∧ ∀ 𝑦 ∈ 𝑥 ∃ 𝑟 ∈ ℝ+ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑥 ) )
94 5 91 93 sylanbrc ⊢ ( 𝑥 ∈ ( ordTop ‘ ≤ ) → 𝑥 ∈ 𝐽 )
95 94 ssriv ⊢ ( ordTop ‘ ≤ ) ⊆ 𝐽