MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xrsmopn Structured version   Visualization version   GIF version

Theorem xrsmopn 24213
Description: The metric on the extended reals generates a topology, but this does not match the order topology on ℝ*; for example {+∞} 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.)
Hypotheses
Ref Expression
xrsxmet.1 𝐷 = (distβ€˜β„*𝑠)
xrsmopn.1 𝐽 = (MetOpenβ€˜π·)
Assertion
Ref Expression
xrsmopn (ordTopβ€˜ ≀ ) βŠ† 𝐽

Proof of Theorem xrsmopn
Dummy variables π‘₯ π‘Ÿ 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elssuni 4904 . . . 4 (π‘₯ ∈ (ordTopβ€˜ ≀ ) β†’ π‘₯ βŠ† βˆͺ (ordTopβ€˜ ≀ ))
2 letopuni 22596 . . . 4 ℝ* = βˆͺ (ordTopβ€˜ ≀ )
31, 2sseqtrrdi 3999 . . 3 (π‘₯ ∈ (ordTopβ€˜ ≀ ) β†’ π‘₯ βŠ† ℝ*)
4 eqid 2732 . . . . . . . 8 ((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)) = ((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ))
54rexmet 24192 . . . . . . 7 ((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)) ∈ (∞Metβ€˜β„)
6 letop 22595 . . . . . . . . 9 (ordTopβ€˜ ≀ ) ∈ Top
7 reex 11152 . . . . . . . . 9 ℝ ∈ V
8 elrestr 17325 . . . . . . . . 9 (((ordTopβ€˜ ≀ ) ∈ Top ∧ ℝ ∈ V ∧ π‘₯ ∈ (ordTopβ€˜ ≀ )) β†’ (π‘₯ ∩ ℝ) ∈ ((ordTopβ€˜ ≀ ) β†Ύt ℝ))
96, 7, 8mp3an12 1452 . . . . . . . 8 (π‘₯ ∈ (ordTopβ€˜ ≀ ) β†’ (π‘₯ ∩ ℝ) ∈ ((ordTopβ€˜ ≀ ) β†Ύt ℝ))
109ad2antrr 725 . . . . . . 7 (((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ 𝑦 ∈ ℝ) β†’ (π‘₯ ∩ ℝ) ∈ ((ordTopβ€˜ ≀ ) β†Ύt ℝ))
11 elin 3930 . . . . . . . . 9 (𝑦 ∈ (π‘₯ ∩ ℝ) ↔ (𝑦 ∈ π‘₯ ∧ 𝑦 ∈ ℝ))
1211biimpri 227 . . . . . . . 8 ((𝑦 ∈ π‘₯ ∧ 𝑦 ∈ ℝ) β†’ 𝑦 ∈ (π‘₯ ∩ ℝ))
1312adantll 713 . . . . . . 7 (((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ 𝑦 ∈ ℝ) β†’ 𝑦 ∈ (π‘₯ ∩ ℝ))
14 eqid 2732 . . . . . . . . . 10 ((ordTopβ€˜ ≀ ) β†Ύt ℝ) = ((ordTopβ€˜ ≀ ) β†Ύt ℝ)
1514xrtgioo 24207 . . . . . . . . 9 (topGenβ€˜ran (,)) = ((ordTopβ€˜ ≀ ) β†Ύt ℝ)
16 eqid 2732 . . . . . . . . . 10 (MetOpenβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ))) = (MetOpenβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))
174, 16tgioo 24197 . . . . . . . . 9 (topGenβ€˜ran (,)) = (MetOpenβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))
1815, 17eqtr3i 2762 . . . . . . . 8 ((ordTopβ€˜ ≀ ) β†Ύt ℝ) = (MetOpenβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))
1918mopni2 23887 . . . . . . 7 ((((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)) ∈ (∞Metβ€˜β„) ∧ (π‘₯ ∩ ℝ) ∈ ((ordTopβ€˜ ≀ ) β†Ύt ℝ) ∧ 𝑦 ∈ (π‘₯ ∩ ℝ)) β†’ βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))π‘Ÿ) βŠ† (π‘₯ ∩ ℝ))
205, 10, 13, 19mp3an2i 1467 . . . . . 6 (((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ 𝑦 ∈ ℝ) β†’ βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))π‘Ÿ) βŠ† (π‘₯ ∩ ℝ))
21 xrsxmet.1 . . . . . . . . . . . 12 𝐷 = (distβ€˜β„*𝑠)
2221xrsxmet 24210 . . . . . . . . . . 11 𝐷 ∈ (∞Metβ€˜β„*)
23 simplr 768 . . . . . . . . . . . 12 ((((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ 𝑦 ∈ ℝ) ∧ π‘Ÿ ∈ ℝ+) β†’ 𝑦 ∈ ℝ)
24 ressxr 11209 . . . . . . . . . . . . 13 ℝ βŠ† ℝ*
25 sseqin2 4181 . . . . . . . . . . . . 13 (ℝ βŠ† ℝ* ↔ (ℝ* ∩ ℝ) = ℝ)
2624, 25mpbi 229 . . . . . . . . . . . 12 (ℝ* ∩ ℝ) = ℝ
2723, 26eleqtrrdi 2844 . . . . . . . . . . 11 ((((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ 𝑦 ∈ ℝ) ∧ π‘Ÿ ∈ ℝ+) β†’ 𝑦 ∈ (ℝ* ∩ ℝ))
28 rpxr 12934 . . . . . . . . . . . 12 (π‘Ÿ ∈ ℝ+ β†’ π‘Ÿ ∈ ℝ*)
2928adantl 483 . . . . . . . . . . 11 ((((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ 𝑦 ∈ ℝ) ∧ π‘Ÿ ∈ ℝ+) β†’ π‘Ÿ ∈ ℝ*)
3021xrsdsre 24211 . . . . . . . . . . . . 13 (𝐷 β†Ύ (ℝ Γ— ℝ)) = ((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ))
3130eqcomi 2741 . . . . . . . . . . . 12 ((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)) = (𝐷 β†Ύ (ℝ Γ— ℝ))
3231blres 23822 . . . . . . . . . . 11 ((𝐷 ∈ (∞Metβ€˜β„*) ∧ 𝑦 ∈ (ℝ* ∩ ℝ) ∧ π‘Ÿ ∈ ℝ*) β†’ (𝑦(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))π‘Ÿ) = ((𝑦(ballβ€˜π·)π‘Ÿ) ∩ ℝ))
3322, 27, 29, 32mp3an2i 1467 . . . . . . . . . 10 ((((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ 𝑦 ∈ ℝ) ∧ π‘Ÿ ∈ ℝ+) β†’ (𝑦(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))π‘Ÿ) = ((𝑦(ballβ€˜π·)π‘Ÿ) ∩ ℝ))
3421xrsblre 24212 . . . . . . . . . . . . 13 ((𝑦 ∈ ℝ ∧ π‘Ÿ ∈ ℝ*) β†’ (𝑦(ballβ€˜π·)π‘Ÿ) βŠ† ℝ)
3528, 34sylan2 594 . . . . . . . . . . . 12 ((𝑦 ∈ ℝ ∧ π‘Ÿ ∈ ℝ+) β†’ (𝑦(ballβ€˜π·)π‘Ÿ) βŠ† ℝ)
3635adantll 713 . . . . . . . . . . 11 ((((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ 𝑦 ∈ ℝ) ∧ π‘Ÿ ∈ ℝ+) β†’ (𝑦(ballβ€˜π·)π‘Ÿ) βŠ† ℝ)
37 df-ss 3931 . . . . . . . . . . 11 ((𝑦(ballβ€˜π·)π‘Ÿ) βŠ† ℝ ↔ ((𝑦(ballβ€˜π·)π‘Ÿ) ∩ ℝ) = (𝑦(ballβ€˜π·)π‘Ÿ))
3836, 37sylib 217 . . . . . . . . . 10 ((((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ 𝑦 ∈ ℝ) ∧ π‘Ÿ ∈ ℝ+) β†’ ((𝑦(ballβ€˜π·)π‘Ÿ) ∩ ℝ) = (𝑦(ballβ€˜π·)π‘Ÿ))
3933, 38eqtrd 2772 . . . . . . . . 9 ((((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ 𝑦 ∈ ℝ) ∧ π‘Ÿ ∈ ℝ+) β†’ (𝑦(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))π‘Ÿ) = (𝑦(ballβ€˜π·)π‘Ÿ))
4039sseq1d 3979 . . . . . . . 8 ((((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ 𝑦 ∈ ℝ) ∧ π‘Ÿ ∈ ℝ+) β†’ ((𝑦(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))π‘Ÿ) βŠ† (π‘₯ ∩ ℝ) ↔ (𝑦(ballβ€˜π·)π‘Ÿ) βŠ† (π‘₯ ∩ ℝ)))
41 inss1 4194 . . . . . . . . 9 (π‘₯ ∩ ℝ) βŠ† π‘₯
42 sstr 3956 . . . . . . . . 9 (((𝑦(ballβ€˜π·)π‘Ÿ) βŠ† (π‘₯ ∩ ℝ) ∧ (π‘₯ ∩ ℝ) βŠ† π‘₯) β†’ (𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯)
4341, 42mpan2 690 . . . . . . . 8 ((𝑦(ballβ€˜π·)π‘Ÿ) βŠ† (π‘₯ ∩ ℝ) β†’ (𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯)
4440, 43syl6bi 253 . . . . . . 7 ((((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ 𝑦 ∈ ℝ) ∧ π‘Ÿ ∈ ℝ+) β†’ ((𝑦(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))π‘Ÿ) βŠ† (π‘₯ ∩ ℝ) β†’ (𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯))
4544reximdva 3162 . . . . . 6 (((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ 𝑦 ∈ ℝ) β†’ (βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))π‘Ÿ) βŠ† (π‘₯ ∩ ℝ) β†’ βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯))
4620, 45mpd 15 . . . . 5 (((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ 𝑦 ∈ ℝ) β†’ βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯)
47 1rp 12929 . . . . . 6 1 ∈ ℝ+
483sselda 3948 . . . . . . . . . 10 ((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) β†’ 𝑦 ∈ ℝ*)
4948adantr 482 . . . . . . . . 9 (((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ Β¬ 𝑦 ∈ ℝ) β†’ 𝑦 ∈ ℝ*)
50 rpxr 12934 . . . . . . . . . 10 (1 ∈ ℝ+ β†’ 1 ∈ ℝ*)
5147, 50mp1i 13 . . . . . . . . 9 (((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ Β¬ 𝑦 ∈ ℝ) β†’ 1 ∈ ℝ*)
52 elbl 23779 . . . . . . . . 9 ((𝐷 ∈ (∞Metβ€˜β„*) ∧ 𝑦 ∈ ℝ* ∧ 1 ∈ ℝ*) β†’ (𝑧 ∈ (𝑦(ballβ€˜π·)1) ↔ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)))
5322, 49, 51, 52mp3an2i 1467 . . . . . . . 8 (((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ Β¬ 𝑦 ∈ ℝ) β†’ (𝑧 ∈ (𝑦(ballβ€˜π·)1) ↔ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)))
54 simp2 1138 . . . . . . . . . 10 (((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ Β¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) β†’ Β¬ 𝑦 ∈ ℝ)
55483ad2ant1 1134 . . . . . . . . . . . . . . . . . 18 (((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ Β¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) β†’ 𝑦 ∈ ℝ*)
5655adantr 482 . . . . . . . . . . . . . . . . 17 ((((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ Β¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 β‰  𝑧) β†’ 𝑦 ∈ ℝ*)
57 simpl3l 1229 . . . . . . . . . . . . . . . . 17 ((((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ Β¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 β‰  𝑧) β†’ 𝑧 ∈ ℝ*)
58 xmetcl 23722 . . . . . . . . . . . . . . . . 17 ((𝐷 ∈ (∞Metβ€˜β„*) ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ*) β†’ (𝑦𝐷𝑧) ∈ ℝ*)
5922, 56, 57, 58mp3an2i 1467 . . . . . . . . . . . . . . . 16 ((((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ Β¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 β‰  𝑧) β†’ (𝑦𝐷𝑧) ∈ ℝ*)
60 1red 11166 . . . . . . . . . . . . . . . 16 ((((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ Β¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 β‰  𝑧) β†’ 1 ∈ ℝ)
61 xmetge0 23735 . . . . . . . . . . . . . . . . 17 ((𝐷 ∈ (∞Metβ€˜β„*) ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ*) β†’ 0 ≀ (𝑦𝐷𝑧))
6222, 56, 57, 61mp3an2i 1467 . . . . . . . . . . . . . . . 16 ((((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ Β¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 β‰  𝑧) β†’ 0 ≀ (𝑦𝐷𝑧))
63 simpl3r 1230 . . . . . . . . . . . . . . . . 17 ((((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ Β¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 β‰  𝑧) β†’ (𝑦𝐷𝑧) < 1)
64 1xr 11224 . . . . . . . . . . . . . . . . . 18 1 ∈ ℝ*
65 xrltle 13079 . . . . . . . . . . . . . . . . . 18 (((𝑦𝐷𝑧) ∈ ℝ* ∧ 1 ∈ ℝ*) β†’ ((𝑦𝐷𝑧) < 1 β†’ (𝑦𝐷𝑧) ≀ 1))
6659, 64, 65sylancl 587 . . . . . . . . . . . . . . . . 17 ((((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ Β¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 β‰  𝑧) β†’ ((𝑦𝐷𝑧) < 1 β†’ (𝑦𝐷𝑧) ≀ 1))
6763, 66mpd 15 . . . . . . . . . . . . . . . 16 ((((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ Β¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 β‰  𝑧) β†’ (𝑦𝐷𝑧) ≀ 1)
68 xrrege0 13104 . . . . . . . . . . . . . . . 16 ((((𝑦𝐷𝑧) ∈ ℝ* ∧ 1 ∈ ℝ) ∧ (0 ≀ (𝑦𝐷𝑧) ∧ (𝑦𝐷𝑧) ≀ 1)) β†’ (𝑦𝐷𝑧) ∈ ℝ)
6959, 60, 62, 67, 68syl22anc 838 . . . . . . . . . . . . . . 15 ((((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ Β¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 β‰  𝑧) β†’ (𝑦𝐷𝑧) ∈ ℝ)
70 simpr 486 . . . . . . . . . . . . . . . 16 ((((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ Β¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 β‰  𝑧) β†’ 𝑦 β‰  𝑧)
7121xrsdsreclb 20882 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ∧ 𝑦 β‰  𝑧) β†’ ((𝑦𝐷𝑧) ∈ ℝ ↔ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)))
7256, 57, 70, 71syl3anc 1372 . . . . . . . . . . . . . . 15 ((((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ Β¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 β‰  𝑧) β†’ ((𝑦𝐷𝑧) ∈ ℝ ↔ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)))
7369, 72mpbid 231 . . . . . . . . . . . . . 14 ((((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ Β¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 β‰  𝑧) β†’ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ))
7473simpld 496 . . . . . . . . . . . . 13 ((((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ Β¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 β‰  𝑧) β†’ 𝑦 ∈ ℝ)
7574ex 414 . . . . . . . . . . . 12 (((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ Β¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) β†’ (𝑦 β‰  𝑧 β†’ 𝑦 ∈ ℝ))
7675necon1bd 2958 . . . . . . . . . . 11 (((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ Β¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) β†’ (Β¬ 𝑦 ∈ ℝ β†’ 𝑦 = 𝑧))
77 simp1r 1199 . . . . . . . . . . . 12 (((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ Β¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) β†’ 𝑦 ∈ π‘₯)
78 elequ1 2114 . . . . . . . . . . . 12 (𝑦 = 𝑧 β†’ (𝑦 ∈ π‘₯ ↔ 𝑧 ∈ π‘₯))
7977, 78syl5ibcom 244 . . . . . . . . . . 11 (((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ Β¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) β†’ (𝑦 = 𝑧 β†’ 𝑧 ∈ π‘₯))
8076, 79syld 47 . . . . . . . . . 10 (((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ Β¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) β†’ (Β¬ 𝑦 ∈ ℝ β†’ 𝑧 ∈ π‘₯))
8154, 80mpd 15 . . . . . . . . 9 (((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ Β¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) β†’ 𝑧 ∈ π‘₯)
82813expia 1122 . . . . . . . 8 (((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ Β¬ 𝑦 ∈ ℝ) β†’ ((𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1) β†’ 𝑧 ∈ π‘₯))
8353, 82sylbid 239 . . . . . . 7 (((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ Β¬ 𝑦 ∈ ℝ) β†’ (𝑧 ∈ (𝑦(ballβ€˜π·)1) β†’ 𝑧 ∈ π‘₯))
8483ssrdv 3954 . . . . . 6 (((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ Β¬ 𝑦 ∈ ℝ) β†’ (𝑦(ballβ€˜π·)1) βŠ† π‘₯)
85 oveq2 7371 . . . . . . . 8 (π‘Ÿ = 1 β†’ (𝑦(ballβ€˜π·)π‘Ÿ) = (𝑦(ballβ€˜π·)1))
8685sseq1d 3979 . . . . . . 7 (π‘Ÿ = 1 β†’ ((𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯ ↔ (𝑦(ballβ€˜π·)1) βŠ† π‘₯))
8786rspcev 3583 . . . . . 6 ((1 ∈ ℝ+ ∧ (𝑦(ballβ€˜π·)1) βŠ† π‘₯) β†’ βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯)
8847, 84, 87sylancr 588 . . . . 5 (((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) ∧ Β¬ 𝑦 ∈ ℝ) β†’ βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯)
8946, 88pm2.61dan 812 . . . 4 ((π‘₯ ∈ (ordTopβ€˜ ≀ ) ∧ 𝑦 ∈ π‘₯) β†’ βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯)
9089ralrimiva 3140 . . 3 (π‘₯ ∈ (ordTopβ€˜ ≀ ) β†’ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯)
91 xrsmopn.1 . . . . 5 𝐽 = (MetOpenβ€˜π·)
9291elmopn2 23836 . . . 4 (𝐷 ∈ (∞Metβ€˜β„*) β†’ (π‘₯ ∈ 𝐽 ↔ (π‘₯ βŠ† ℝ* ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯)))
9322, 92ax-mp 5 . . 3 (π‘₯ ∈ 𝐽 ↔ (π‘₯ βŠ† ℝ* ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯))
943, 90, 93sylanbrc 584 . 2 (π‘₯ ∈ (ordTopβ€˜ ≀ ) β†’ π‘₯ ∈ 𝐽)
9594ssriv 3952 1 (ordTopβ€˜ ≀ ) βŠ† 𝐽
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  Vcvv 3447   ∩ cin 3913   βŠ† wss 3914  βˆͺ cuni 4871   class class class wbr 5111   Γ— cxp 5637  ran crn 5640   β†Ύ cres 5641   ∘ ccom 5643  β€˜cfv 6502  (class class class)co 7363  β„cr 11060  0cc0 11061  1c1 11062  β„*cxr 11198   < clt 11199   ≀ cle 11200   βˆ’ cmin 11395  β„+crp 12925  (,)cioo 13275  abscabs 15132  distcds 17157   β†Ύt crest 17317  topGenctg 17334  ordTopcordt 17396  β„*𝑠cxrs 17397  βˆžMetcxmet 20819  ballcbl 20821  MetOpencmopn 20824  Topctop 22280
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2703  ax-rep 5248  ax-sep 5262  ax-nul 5269  ax-pow 5326  ax-pr 5390  ax-un 7678  ax-cnex 11117  ax-resscn 11118  ax-1cn 11119  ax-icn 11120  ax-addcl 11121  ax-addrcl 11122  ax-mulcl 11123  ax-mulrcl 11124  ax-mulcom 11125  ax-addass 11126  ax-mulass 11127  ax-distr 11128  ax-i2m1 11129  ax-1ne0 11130  ax-1rid 11131  ax-rnegex 11132  ax-rrecex 11133  ax-cnre 11134  ax-pre-lttri 11135  ax-pre-lttrn 11136  ax-pre-ltadd 11137  ax-pre-mulgt0 11138  ax-pre-sup 11139
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3933  df-nul 4289  df-if 4493  df-pw 4568  df-sn 4593  df-pr 4595  df-tp 4597  df-op 4599  df-uni 4872  df-int 4914  df-iun 4962  df-br 5112  df-opab 5174  df-mpt 5195  df-tr 5229  df-id 5537  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5594  df-we 5596  df-xp 5645  df-rel 5646  df-cnv 5647  df-co 5648  df-dm 5649  df-rn 5650  df-res 5651  df-ima 5652  df-pred 6259  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-riota 7319  df-ov 7366  df-oprab 7367  df-mpo 7368  df-om 7809  df-1st 7927  df-2nd 7928  df-frecs 8218  df-wrecs 8249  df-recs 8323  df-rdg 8362  df-1o 8418  df-er 8656  df-ec 8658  df-map 8775  df-en 8892  df-dom 8893  df-sdom 8894  df-fin 8895  df-fi 9357  df-sup 9388  df-inf 9389  df-pnf 11201  df-mnf 11202  df-xr 11203  df-ltxr 11204  df-le 11205  df-sub 11397  df-neg 11398  df-div 11823  df-nn 12164  df-2 12226  df-3 12227  df-4 12228  df-5 12229  df-6 12230  df-7 12231  df-8 12232  df-9 12233  df-n0 12424  df-z 12510  df-dec 12629  df-uz 12774  df-q 12884  df-rp 12926  df-xneg 13043  df-xadd 13044  df-xmul 13045  df-ioo 13279  df-ioc 13280  df-ico 13281  df-icc 13282  df-fz 13436  df-seq 13918  df-exp 13979  df-cj 14997  df-re 14998  df-im 14999  df-sqrt 15133  df-abs 15134  df-struct 17031  df-slot 17066  df-ndx 17078  df-base 17096  df-plusg 17161  df-mulr 17162  df-tset 17167  df-ple 17168  df-ds 17170  df-rest 17319  df-topgen 17340  df-ordt 17398  df-xrs 17399  df-ps 18470  df-tsr 18471  df-psmet 20826  df-xmet 20827  df-met 20828  df-bl 20829  df-mopn 20830  df-top 22281  df-topon 22298  df-bases 22334
This theorem is referenced by:  xmetdcn  24239
  Copyright terms: Public domain W3C validator