| Step | Hyp | Ref
| Expression |
| 1 | | elssuni 4937 |
. . . 4
⊢ (𝑥 ∈ (ordTop‘ ≤ )
→ 𝑥 ⊆ ∪ (ordTop‘ ≤ )) |
| 2 | | letopuni 23215 |
. . . 4
⊢
ℝ* = ∪ (ordTop‘ ≤
) |
| 3 | 1, 2 | sseqtrrdi 4025 |
. . 3
⊢ (𝑥 ∈ (ordTop‘ ≤ )
→ 𝑥 ⊆
ℝ*) |
| 4 | | eqid 2737 |
. . . . . . . 8
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − )
↾ (ℝ × ℝ)) |
| 5 | 4 | rexmet 24812 |
. . . . . . 7
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) |
| 6 | | letop 23214 |
. . . . . . . . 9
⊢
(ordTop‘ ≤ ) ∈ Top |
| 7 | | reex 11246 |
. . . . . . . . 9
⊢ ℝ
∈ V |
| 8 | | elrestr 17473 |
. . . . . . . . 9
⊢
(((ordTop‘ ≤ ) ∈ Top ∧ ℝ ∈ V ∧ 𝑥 ∈ (ordTop‘ ≤ ))
→ (𝑥 ∩ ℝ)
∈ ((ordTop‘ ≤ ) ↾t ℝ)) |
| 9 | 6, 7, 8 | mp3an12 1453 |
. . . . . . . 8
⊢ (𝑥 ∈ (ordTop‘ ≤ )
→ (𝑥 ∩ ℝ)
∈ ((ordTop‘ ≤ ) ↾t ℝ)) |
| 10 | 9 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) → (𝑥 ∩ ℝ) ∈ ((ordTop‘ ≤ )
↾t ℝ)) |
| 11 | | elin 3967 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝑥 ∩ ℝ) ↔ (𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ℝ)) |
| 12 | 11 | biimpri 228 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ (𝑥 ∩ ℝ)) |
| 13 | 12 | adantll 714 |
. . . . . . 7
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ (𝑥 ∩ ℝ)) |
| 14 | | eqid 2737 |
. . . . . . . . . 10
⊢
((ordTop‘ ≤ ) ↾t ℝ) = ((ordTop‘
≤ ) ↾t ℝ) |
| 15 | 14 | xrtgioo 24828 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) = ((ordTop‘ ≤ ) ↾t
ℝ) |
| 16 | | eqid 2737 |
. . . . . . . . . 10
⊢
(MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) |
| 17 | 4, 16 | tgioo 24817 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾
(ℝ × ℝ))) |
| 18 | 15, 17 | eqtr3i 2767 |
. . . . . . . 8
⊢
((ordTop‘ ≤ ) ↾t ℝ) =
(MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) |
| 19 | 18 | mopni2 24506 |
. . . . . . 7
⊢ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) ∧ (𝑥 ∩ ℝ) ∈ ((ordTop‘ ≤ )
↾t ℝ) ∧ 𝑦 ∈ (𝑥 ∩ ℝ)) → ∃𝑟 ∈ ℝ+
(𝑦(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑥 ∩ ℝ)) |
| 20 | 5, 10, 13, 19 | mp3an2i 1468 |
. . . . . 6
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) → ∃𝑟 ∈ ℝ+
(𝑦(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑥 ∩ ℝ)) |
| 21 | | xrsxmet.1 |
. . . . . . . . . . . 12
⊢ 𝐷 =
(dist‘ℝ*𝑠) |
| 22 | 21 | xrsxmet 24831 |
. . . . . . . . . . 11
⊢ 𝐷 ∈
(∞Met‘ℝ*) |
| 23 | | simplr 769 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → 𝑦 ∈
ℝ) |
| 24 | | ressxr 11305 |
. . . . . . . . . . . . 13
⊢ ℝ
⊆ ℝ* |
| 25 | | sseqin2 4223 |
. . . . . . . . . . . . 13
⊢ (ℝ
⊆ ℝ* ↔ (ℝ* ∩ ℝ) =
ℝ) |
| 26 | 24, 25 | mpbi 230 |
. . . . . . . . . . . 12
⊢
(ℝ* ∩ ℝ) = ℝ |
| 27 | 23, 26 | eleqtrrdi 2852 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → 𝑦 ∈ (ℝ*
∩ ℝ)) |
| 28 | | rpxr 13044 |
. . . . . . . . . . . 12
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ*) |
| 29 | 28 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈
ℝ*) |
| 30 | 21 | xrsdsre 24832 |
. . . . . . . . . . . . 13
⊢ (𝐷 ↾ (ℝ ×
ℝ)) = ((abs ∘ − ) ↾ (ℝ ×
ℝ)) |
| 31 | 30 | eqcomi 2746 |
. . . . . . . . . . . 12
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) = (𝐷 ↾ (ℝ ×
ℝ)) |
| 32 | 31 | blres 24441 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈
(∞Met‘ℝ*) ∧ 𝑦 ∈ (ℝ* ∩ ℝ)
∧ 𝑟 ∈
ℝ*) → (𝑦(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) = ((𝑦(ball‘𝐷)𝑟) ∩ ℝ)) |
| 33 | 22, 27, 29, 32 | mp3an2i 1468 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → (𝑦(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) = ((𝑦(ball‘𝐷)𝑟) ∩ ℝ)) |
| 34 | 21 | xrsblre 24833 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℝ ∧ 𝑟 ∈ ℝ*)
→ (𝑦(ball‘𝐷)𝑟) ⊆ ℝ) |
| 35 | 28, 34 | sylan2 593 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℝ ∧ 𝑟 ∈ ℝ+)
→ (𝑦(ball‘𝐷)𝑟) ⊆ ℝ) |
| 36 | 35 | adantll 714 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → (𝑦(ball‘𝐷)𝑟) ⊆ ℝ) |
| 37 | | dfss2 3969 |
. . . . . . . . . . 11
⊢ ((𝑦(ball‘𝐷)𝑟) ⊆ ℝ ↔ ((𝑦(ball‘𝐷)𝑟) ∩ ℝ) = (𝑦(ball‘𝐷)𝑟)) |
| 38 | 36, 37 | sylib 218 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → ((𝑦(ball‘𝐷)𝑟) ∩ ℝ) = (𝑦(ball‘𝐷)𝑟)) |
| 39 | 33, 38 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → (𝑦(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) = (𝑦(ball‘𝐷)𝑟)) |
| 40 | 39 | sseq1d 4015 |
. . . . . . . 8
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → ((𝑦(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑥 ∩ ℝ) ↔ (𝑦(ball‘𝐷)𝑟) ⊆ (𝑥 ∩ ℝ))) |
| 41 | | inss1 4237 |
. . . . . . . . 9
⊢ (𝑥 ∩ ℝ) ⊆ 𝑥 |
| 42 | | sstr 3992 |
. . . . . . . . 9
⊢ (((𝑦(ball‘𝐷)𝑟) ⊆ (𝑥 ∩ ℝ) ∧ (𝑥 ∩ ℝ) ⊆ 𝑥) → (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥) |
| 43 | 41, 42 | mpan2 691 |
. . . . . . . 8
⊢ ((𝑦(ball‘𝐷)𝑟) ⊆ (𝑥 ∩ ℝ) → (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥) |
| 44 | 40, 43 | biimtrdi 253 |
. . . . . . 7
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → ((𝑦(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑥 ∩ ℝ) → (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)) |
| 45 | 44 | reximdva 3168 |
. . . . . 6
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) → (∃𝑟 ∈ ℝ+
(𝑦(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑥 ∩ ℝ) → ∃𝑟 ∈ ℝ+
(𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)) |
| 46 | 20, 45 | mpd 15 |
. . . . 5
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) → ∃𝑟 ∈ ℝ+
(𝑦(ball‘𝐷)𝑟) ⊆ 𝑥) |
| 47 | | 1rp 13038 |
. . . . . 6
⊢ 1 ∈
ℝ+ |
| 48 | 3 | sselda 3983 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ ℝ*) |
| 49 | 48 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ*) |
| 50 | | rpxr 13044 |
. . . . . . . . . 10
⊢ (1 ∈
ℝ+ → 1 ∈ ℝ*) |
| 51 | 47, 50 | mp1i 13 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → 1 ∈
ℝ*) |
| 52 | | elbl 24398 |
. . . . . . . . 9
⊢ ((𝐷 ∈
(∞Met‘ℝ*) ∧ 𝑦 ∈ ℝ* ∧ 1 ∈
ℝ*) → (𝑧 ∈ (𝑦(ball‘𝐷)1) ↔ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1))) |
| 53 | 22, 49, 51, 52 | mp3an2i 1468 |
. . . . . . . 8
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → (𝑧 ∈ (𝑦(ball‘𝐷)1) ↔ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1))) |
| 54 | | simp2 1138 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) → ¬ 𝑦 ∈ ℝ) |
| 55 | 48 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) → 𝑦 ∈ ℝ*) |
| 56 | 55 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → 𝑦 ∈ ℝ*) |
| 57 | | simpl3l 1229 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → 𝑧 ∈ ℝ*) |
| 58 | | xmetcl 24341 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈
(∞Met‘ℝ*) ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ*)
→ (𝑦𝐷𝑧) ∈
ℝ*) |
| 59 | 22, 56, 57, 58 | mp3an2i 1468 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → (𝑦𝐷𝑧) ∈
ℝ*) |
| 60 | | 1red 11262 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → 1 ∈ ℝ) |
| 61 | | xmetge0 24354 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈
(∞Met‘ℝ*) ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ*)
→ 0 ≤ (𝑦𝐷𝑧)) |
| 62 | 22, 56, 57, 61 | mp3an2i 1468 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → 0 ≤ (𝑦𝐷𝑧)) |
| 63 | | simpl3r 1230 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → (𝑦𝐷𝑧) < 1) |
| 64 | | 1xr 11320 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℝ* |
| 65 | | xrltle 13191 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦𝐷𝑧) ∈ ℝ* ∧ 1 ∈
ℝ*) → ((𝑦𝐷𝑧) < 1 → (𝑦𝐷𝑧) ≤ 1)) |
| 66 | 59, 64, 65 | sylancl 586 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → ((𝑦𝐷𝑧) < 1 → (𝑦𝐷𝑧) ≤ 1)) |
| 67 | 63, 66 | mpd 15 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → (𝑦𝐷𝑧) ≤ 1) |
| 68 | | xrrege0 13216 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑦𝐷𝑧) ∈ ℝ* ∧ 1 ∈
ℝ) ∧ (0 ≤ (𝑦𝐷𝑧) ∧ (𝑦𝐷𝑧) ≤ 1)) → (𝑦𝐷𝑧) ∈ ℝ) |
| 69 | 59, 60, 62, 67, 68 | syl22anc 839 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → (𝑦𝐷𝑧) ∈ ℝ) |
| 70 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → 𝑦 ≠ 𝑧) |
| 71 | 21 | xrsdsreclb 21431 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℝ*
∧ 𝑧 ∈
ℝ* ∧ 𝑦
≠ 𝑧) → ((𝑦𝐷𝑧) ∈ ℝ ↔ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ))) |
| 72 | 56, 57, 70, 71 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → ((𝑦𝐷𝑧) ∈ ℝ ↔ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ))) |
| 73 | 69, 72 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) |
| 74 | 73 | simpld 494 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → 𝑦 ∈ ℝ) |
| 75 | 74 | ex 412 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) → (𝑦 ≠ 𝑧 → 𝑦 ∈ ℝ)) |
| 76 | 75 | necon1bd 2958 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) → (¬ 𝑦 ∈ ℝ → 𝑦 = 𝑧)) |
| 77 | | simp1r 1199 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) → 𝑦 ∈ 𝑥) |
| 78 | | elequ1 2115 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → (𝑦 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥)) |
| 79 | 77, 78 | syl5ibcom 245 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) → (𝑦 = 𝑧 → 𝑧 ∈ 𝑥)) |
| 80 | 76, 79 | syld 47 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) → (¬ 𝑦 ∈ ℝ → 𝑧 ∈ 𝑥)) |
| 81 | 54, 80 | mpd 15 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) → 𝑧 ∈ 𝑥) |
| 82 | 81 | 3expia 1122 |
. . . . . . . 8
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → ((𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1) → 𝑧 ∈ 𝑥)) |
| 83 | 53, 82 | sylbid 240 |
. . . . . . 7
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → (𝑧 ∈ (𝑦(ball‘𝐷)1) → 𝑧 ∈ 𝑥)) |
| 84 | 83 | ssrdv 3989 |
. . . . . 6
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → (𝑦(ball‘𝐷)1) ⊆ 𝑥) |
| 85 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑟 = 1 → (𝑦(ball‘𝐷)𝑟) = (𝑦(ball‘𝐷)1)) |
| 86 | 85 | sseq1d 4015 |
. . . . . . 7
⊢ (𝑟 = 1 → ((𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ (𝑦(ball‘𝐷)1) ⊆ 𝑥)) |
| 87 | 86 | rspcev 3622 |
. . . . . 6
⊢ ((1
∈ ℝ+ ∧ (𝑦(ball‘𝐷)1) ⊆ 𝑥) → ∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥) |
| 88 | 47, 84, 87 | sylancr 587 |
. . . . 5
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → ∃𝑟 ∈ ℝ+
(𝑦(ball‘𝐷)𝑟) ⊆ 𝑥) |
| 89 | 46, 88 | pm2.61dan 813 |
. . . 4
⊢ ((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) → ∃𝑟 ∈ ℝ+
(𝑦(ball‘𝐷)𝑟) ⊆ 𝑥) |
| 90 | 89 | ralrimiva 3146 |
. . 3
⊢ (𝑥 ∈ (ordTop‘ ≤ )
→ ∀𝑦 ∈
𝑥 ∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥) |
| 91 | | xrsmopn.1 |
. . . . 5
⊢ 𝐽 = (MetOpen‘𝐷) |
| 92 | 91 | elmopn2 24455 |
. . . 4
⊢ (𝐷 ∈
(∞Met‘ℝ*) → (𝑥 ∈ 𝐽 ↔ (𝑥 ⊆ ℝ* ∧
∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥))) |
| 93 | 22, 92 | ax-mp 5 |
. . 3
⊢ (𝑥 ∈ 𝐽 ↔ (𝑥 ⊆ ℝ* ∧
∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)) |
| 94 | 3, 90, 93 | sylanbrc 583 |
. 2
⊢ (𝑥 ∈ (ordTop‘ ≤ )
→ 𝑥 ∈ 𝐽) |
| 95 | 94 | ssriv 3987 |
1
⊢
(ordTop‘ ≤ ) ⊆ 𝐽 |