Step | Hyp | Ref
| Expression |
1 | | elssuni 4403 |
. . . 4
⊢ (𝑥 ∈ (ordTop‘ ≤ )
→ 𝑥 ⊆ ∪ (ordTop‘ ≤ )) |
2 | | letopuni 20821 |
. . . 4
⊢
ℝ* = ∪ (ordTop‘ ≤
) |
3 | 1, 2 | syl6sseqr 3615 |
. . 3
⊢ (𝑥 ∈ (ordTop‘ ≤ )
→ 𝑥 ⊆
ℝ*) |
4 | | eqid 2610 |
. . . . . . . . 9
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − )
↾ (ℝ × ℝ)) |
5 | 4 | rexmet 22402 |
. . . . . . . 8
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) |
6 | 5 | a1i 11 |
. . . . . . 7
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) → ((abs ∘ −
) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ)) |
7 | | letop 20820 |
. . . . . . . . 9
⊢
(ordTop‘ ≤ ) ∈ Top |
8 | | reex 9906 |
. . . . . . . . 9
⊢ ℝ
∈ V |
9 | | elrestr 15912 |
. . . . . . . . 9
⊢
(((ordTop‘ ≤ ) ∈ Top ∧ ℝ ∈ V ∧ 𝑥 ∈ (ordTop‘ ≤ ))
→ (𝑥 ∩ ℝ)
∈ ((ordTop‘ ≤ ) ↾t ℝ)) |
10 | 7, 8, 9 | mp3an12 1406 |
. . . . . . . 8
⊢ (𝑥 ∈ (ordTop‘ ≤ )
→ (𝑥 ∩ ℝ)
∈ ((ordTop‘ ≤ ) ↾t ℝ)) |
11 | 10 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) → (𝑥 ∩ ℝ) ∈ ((ordTop‘ ≤ )
↾t ℝ)) |
12 | | elin 3758 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝑥 ∩ ℝ) ↔ (𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ℝ)) |
13 | 12 | biimpri 217 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ (𝑥 ∩ ℝ)) |
14 | 13 | adantll 746 |
. . . . . . 7
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ (𝑥 ∩ ℝ)) |
15 | | eqid 2610 |
. . . . . . . . . 10
⊢
((ordTop‘ ≤ ) ↾t ℝ) = ((ordTop‘
≤ ) ↾t ℝ) |
16 | 15 | xrtgioo 22417 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) = ((ordTop‘ ≤ ) ↾t
ℝ) |
17 | | eqid 2610 |
. . . . . . . . . 10
⊢
(MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) |
18 | 4, 17 | tgioo 22407 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾
(ℝ × ℝ))) |
19 | 16, 18 | eqtr3i 2634 |
. . . . . . . 8
⊢
((ordTop‘ ≤ ) ↾t ℝ) =
(MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) |
20 | 19 | mopni2 22108 |
. . . . . . 7
⊢ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) ∧ (𝑥 ∩ ℝ) ∈ ((ordTop‘ ≤ )
↾t ℝ) ∧ 𝑦 ∈ (𝑥 ∩ ℝ)) → ∃𝑟 ∈ ℝ+
(𝑦(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑥 ∩ ℝ)) |
21 | 6, 11, 14, 20 | syl3anc 1318 |
. . . . . 6
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) → ∃𝑟 ∈ ℝ+
(𝑦(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑥 ∩ ℝ)) |
22 | | xrsxmet.1 |
. . . . . . . . . . . . 13
⊢ 𝐷 =
(dist‘ℝ*𝑠) |
23 | 22 | xrsxmet 22420 |
. . . . . . . . . . . 12
⊢ 𝐷 ∈
(∞Met‘ℝ*) |
24 | 23 | a1i 11 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → 𝐷 ∈
(∞Met‘ℝ*)) |
25 | | simplr 788 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → 𝑦 ∈
ℝ) |
26 | | ressxr 9962 |
. . . . . . . . . . . . 13
⊢ ℝ
⊆ ℝ* |
27 | | sseqin2 3779 |
. . . . . . . . . . . . 13
⊢ (ℝ
⊆ ℝ* ↔ (ℝ* ∩ ℝ) =
ℝ) |
28 | 26, 27 | mpbi 219 |
. . . . . . . . . . . 12
⊢
(ℝ* ∩ ℝ) = ℝ |
29 | 25, 28 | syl6eleqr 2699 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → 𝑦 ∈ (ℝ*
∩ ℝ)) |
30 | | rpxr 11716 |
. . . . . . . . . . . 12
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ*) |
31 | 30 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈
ℝ*) |
32 | 22 | xrsdsre 22421 |
. . . . . . . . . . . . 13
⊢ (𝐷 ↾ (ℝ ×
ℝ)) = ((abs ∘ − ) ↾ (ℝ ×
ℝ)) |
33 | 32 | eqcomi 2619 |
. . . . . . . . . . . 12
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) = (𝐷 ↾ (ℝ ×
ℝ)) |
34 | 33 | blres 22046 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈
(∞Met‘ℝ*) ∧ 𝑦 ∈ (ℝ* ∩ ℝ)
∧ 𝑟 ∈
ℝ*) → (𝑦(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) = ((𝑦(ball‘𝐷)𝑟) ∩ ℝ)) |
35 | 24, 29, 31, 34 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → (𝑦(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) = ((𝑦(ball‘𝐷)𝑟) ∩ ℝ)) |
36 | 22 | xrsblre 22422 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℝ ∧ 𝑟 ∈ ℝ*)
→ (𝑦(ball‘𝐷)𝑟) ⊆ ℝ) |
37 | 30, 36 | sylan2 490 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℝ ∧ 𝑟 ∈ ℝ+)
→ (𝑦(ball‘𝐷)𝑟) ⊆ ℝ) |
38 | 37 | adantll 746 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → (𝑦(ball‘𝐷)𝑟) ⊆ ℝ) |
39 | | df-ss 3554 |
. . . . . . . . . . 11
⊢ ((𝑦(ball‘𝐷)𝑟) ⊆ ℝ ↔ ((𝑦(ball‘𝐷)𝑟) ∩ ℝ) = (𝑦(ball‘𝐷)𝑟)) |
40 | 38, 39 | sylib 207 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → ((𝑦(ball‘𝐷)𝑟) ∩ ℝ) = (𝑦(ball‘𝐷)𝑟)) |
41 | 35, 40 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → (𝑦(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) = (𝑦(ball‘𝐷)𝑟)) |
42 | 41 | sseq1d 3595 |
. . . . . . . 8
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → ((𝑦(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑥 ∩ ℝ) ↔ (𝑦(ball‘𝐷)𝑟) ⊆ (𝑥 ∩ ℝ))) |
43 | | inss1 3795 |
. . . . . . . . 9
⊢ (𝑥 ∩ ℝ) ⊆ 𝑥 |
44 | | sstr 3576 |
. . . . . . . . 9
⊢ (((𝑦(ball‘𝐷)𝑟) ⊆ (𝑥 ∩ ℝ) ∧ (𝑥 ∩ ℝ) ⊆ 𝑥) → (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥) |
45 | 43, 44 | mpan2 703 |
. . . . . . . 8
⊢ ((𝑦(ball‘𝐷)𝑟) ⊆ (𝑥 ∩ ℝ) → (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥) |
46 | 42, 45 | syl6bi 242 |
. . . . . . 7
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → ((𝑦(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑥 ∩ ℝ) → (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)) |
47 | 46 | reximdva 3000 |
. . . . . 6
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) → (∃𝑟 ∈ ℝ+
(𝑦(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑥 ∩ ℝ) → ∃𝑟 ∈ ℝ+
(𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)) |
48 | 21, 47 | mpd 15 |
. . . . 5
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) → ∃𝑟 ∈ ℝ+
(𝑦(ball‘𝐷)𝑟) ⊆ 𝑥) |
49 | | 1rp 11712 |
. . . . . 6
⊢ 1 ∈
ℝ+ |
50 | 23 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → 𝐷 ∈
(∞Met‘ℝ*)) |
51 | 3 | sselda 3568 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ ℝ*) |
52 | 51 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ*) |
53 | | rpxr 11716 |
. . . . . . . . . 10
⊢ (1 ∈
ℝ+ → 1 ∈ ℝ*) |
54 | 49, 53 | mp1i 13 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → 1 ∈
ℝ*) |
55 | | elbl 22003 |
. . . . . . . . 9
⊢ ((𝐷 ∈
(∞Met‘ℝ*) ∧ 𝑦 ∈ ℝ* ∧ 1 ∈
ℝ*) → (𝑧 ∈ (𝑦(ball‘𝐷)1) ↔ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1))) |
56 | 50, 52, 54, 55 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → (𝑧 ∈ (𝑦(ball‘𝐷)1) ↔ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1))) |
57 | | simp2 1055 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) → ¬ 𝑦 ∈ ℝ) |
58 | 23 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → 𝐷 ∈
(∞Met‘ℝ*)) |
59 | 51 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) → 𝑦 ∈ ℝ*) |
60 | 59 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → 𝑦 ∈ ℝ*) |
61 | | simpl3l 1109 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → 𝑧 ∈ ℝ*) |
62 | | xmetcl 21946 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈
(∞Met‘ℝ*) ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ*)
→ (𝑦𝐷𝑧) ∈
ℝ*) |
63 | 58, 60, 61, 62 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → (𝑦𝐷𝑧) ∈
ℝ*) |
64 | | 1red 9934 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → 1 ∈ ℝ) |
65 | | xmetge0 21959 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈
(∞Met‘ℝ*) ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ*)
→ 0 ≤ (𝑦𝐷𝑧)) |
66 | 58, 60, 61, 65 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → 0 ≤ (𝑦𝐷𝑧)) |
67 | | simpl3r 1110 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → (𝑦𝐷𝑧) < 1) |
68 | 49, 53 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℝ* |
69 | | xrltle 11858 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦𝐷𝑧) ∈ ℝ* ∧ 1 ∈
ℝ*) → ((𝑦𝐷𝑧) < 1 → (𝑦𝐷𝑧) ≤ 1)) |
70 | 63, 68, 69 | sylancl 693 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → ((𝑦𝐷𝑧) < 1 → (𝑦𝐷𝑧) ≤ 1)) |
71 | 67, 70 | mpd 15 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → (𝑦𝐷𝑧) ≤ 1) |
72 | | xrrege0 11879 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑦𝐷𝑧) ∈ ℝ* ∧ 1 ∈
ℝ) ∧ (0 ≤ (𝑦𝐷𝑧) ∧ (𝑦𝐷𝑧) ≤ 1)) → (𝑦𝐷𝑧) ∈ ℝ) |
73 | 63, 64, 66, 71, 72 | syl22anc 1319 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → (𝑦𝐷𝑧) ∈ ℝ) |
74 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → 𝑦 ≠ 𝑧) |
75 | 22 | xrsdsreclb 19612 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℝ*
∧ 𝑧 ∈
ℝ* ∧ 𝑦
≠ 𝑧) → ((𝑦𝐷𝑧) ∈ ℝ ↔ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ))) |
76 | 60, 61, 74, 75 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → ((𝑦𝐷𝑧) ∈ ℝ ↔ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ))) |
77 | 73, 76 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) |
78 | 77 | simpld 474 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → 𝑦 ∈ ℝ) |
79 | 78 | ex 449 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) → (𝑦 ≠ 𝑧 → 𝑦 ∈ ℝ)) |
80 | 79 | necon1bd 2800 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) → (¬ 𝑦 ∈ ℝ → 𝑦 = 𝑧)) |
81 | | simp1r 1079 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) → 𝑦 ∈ 𝑥) |
82 | | elequ1 1984 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → (𝑦 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥)) |
83 | 81, 82 | syl5ibcom 234 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) → (𝑦 = 𝑧 → 𝑧 ∈ 𝑥)) |
84 | 80, 83 | syld 46 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) → (¬ 𝑦 ∈ ℝ → 𝑧 ∈ 𝑥)) |
85 | 57, 84 | mpd 15 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) → 𝑧 ∈ 𝑥) |
86 | 85 | 3expia 1259 |
. . . . . . . 8
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → ((𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1) → 𝑧 ∈ 𝑥)) |
87 | 56, 86 | sylbid 229 |
. . . . . . 7
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → (𝑧 ∈ (𝑦(ball‘𝐷)1) → 𝑧 ∈ 𝑥)) |
88 | 87 | ssrdv 3574 |
. . . . . 6
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → (𝑦(ball‘𝐷)1) ⊆ 𝑥) |
89 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑟 = 1 → (𝑦(ball‘𝐷)𝑟) = (𝑦(ball‘𝐷)1)) |
90 | 89 | sseq1d 3595 |
. . . . . . 7
⊢ (𝑟 = 1 → ((𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ (𝑦(ball‘𝐷)1) ⊆ 𝑥)) |
91 | 90 | rspcev 3282 |
. . . . . 6
⊢ ((1
∈ ℝ+ ∧ (𝑦(ball‘𝐷)1) ⊆ 𝑥) → ∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥) |
92 | 49, 88, 91 | sylancr 694 |
. . . . 5
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → ∃𝑟 ∈ ℝ+
(𝑦(ball‘𝐷)𝑟) ⊆ 𝑥) |
93 | 48, 92 | pm2.61dan 828 |
. . . 4
⊢ ((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) → ∃𝑟 ∈ ℝ+
(𝑦(ball‘𝐷)𝑟) ⊆ 𝑥) |
94 | 93 | ralrimiva 2949 |
. . 3
⊢ (𝑥 ∈ (ordTop‘ ≤ )
→ ∀𝑦 ∈
𝑥 ∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥) |
95 | | xrsmopn.1 |
. . . . 5
⊢ 𝐽 = (MetOpen‘𝐷) |
96 | 95 | elmopn2 22060 |
. . . 4
⊢ (𝐷 ∈
(∞Met‘ℝ*) → (𝑥 ∈ 𝐽 ↔ (𝑥 ⊆ ℝ* ∧
∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥))) |
97 | 23, 96 | ax-mp 5 |
. . 3
⊢ (𝑥 ∈ 𝐽 ↔ (𝑥 ⊆ ℝ* ∧
∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)) |
98 | 3, 94, 97 | sylanbrc 695 |
. 2
⊢ (𝑥 ∈ (ordTop‘ ≤ )
→ 𝑥 ∈ 𝐽) |
99 | 98 | ssriv 3572 |
1
⊢
(ordTop‘ ≤ ) ⊆ 𝐽 |