Step | Hyp | Ref
| Expression |
1 | | elssuni 4691 |
. . . 4
⊢ (𝑥 ∈ (ordTop‘ ≤ )
→ 𝑥 ⊆ ∪ (ordTop‘ ≤ )) |
2 | | letopuni 21389 |
. . . 4
⊢
ℝ* = ∪ (ordTop‘ ≤
) |
3 | 1, 2 | syl6sseqr 3877 |
. . 3
⊢ (𝑥 ∈ (ordTop‘ ≤ )
→ 𝑥 ⊆
ℝ*) |
4 | | eqid 2825 |
. . . . . . . . 9
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − )
↾ (ℝ × ℝ)) |
5 | 4 | rexmet 22971 |
. . . . . . . 8
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) |
6 | 5 | a1i 11 |
. . . . . . 7
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) → ((abs ∘ −
) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ)) |
7 | | letop 21388 |
. . . . . . . . 9
⊢
(ordTop‘ ≤ ) ∈ Top |
8 | | reex 10350 |
. . . . . . . . 9
⊢ ℝ
∈ V |
9 | | elrestr 16449 |
. . . . . . . . 9
⊢
(((ordTop‘ ≤ ) ∈ Top ∧ ℝ ∈ V ∧ 𝑥 ∈ (ordTop‘ ≤ ))
→ (𝑥 ∩ ℝ)
∈ ((ordTop‘ ≤ ) ↾t ℝ)) |
10 | 7, 8, 9 | mp3an12 1579 |
. . . . . . . 8
⊢ (𝑥 ∈ (ordTop‘ ≤ )
→ (𝑥 ∩ ℝ)
∈ ((ordTop‘ ≤ ) ↾t ℝ)) |
11 | 10 | ad2antrr 717 |
. . . . . . 7
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) → (𝑥 ∩ ℝ) ∈ ((ordTop‘ ≤ )
↾t ℝ)) |
12 | | elin 4025 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝑥 ∩ ℝ) ↔ (𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ℝ)) |
13 | 12 | biimpri 220 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ (𝑥 ∩ ℝ)) |
14 | 13 | adantll 705 |
. . . . . . 7
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ (𝑥 ∩ ℝ)) |
15 | | eqid 2825 |
. . . . . . . . . 10
⊢
((ordTop‘ ≤ ) ↾t ℝ) = ((ordTop‘
≤ ) ↾t ℝ) |
16 | 15 | xrtgioo 22986 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) = ((ordTop‘ ≤ ) ↾t
ℝ) |
17 | | eqid 2825 |
. . . . . . . . . 10
⊢
(MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) |
18 | 4, 17 | tgioo 22976 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾
(ℝ × ℝ))) |
19 | 16, 18 | eqtr3i 2851 |
. . . . . . . 8
⊢
((ordTop‘ ≤ ) ↾t ℝ) =
(MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) |
20 | 19 | mopni2 22675 |
. . . . . . 7
⊢ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) ∧ (𝑥 ∩ ℝ) ∈ ((ordTop‘ ≤ )
↾t ℝ) ∧ 𝑦 ∈ (𝑥 ∩ ℝ)) → ∃𝑟 ∈ ℝ+
(𝑦(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑥 ∩ ℝ)) |
21 | 6, 11, 14, 20 | syl3anc 1494 |
. . . . . 6
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) → ∃𝑟 ∈ ℝ+
(𝑦(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑥 ∩ ℝ)) |
22 | | xrsxmet.1 |
. . . . . . . . . . . . 13
⊢ 𝐷 =
(dist‘ℝ*𝑠) |
23 | 22 | xrsxmet 22989 |
. . . . . . . . . . . 12
⊢ 𝐷 ∈
(∞Met‘ℝ*) |
24 | 23 | a1i 11 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → 𝐷 ∈
(∞Met‘ℝ*)) |
25 | | simplr 785 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → 𝑦 ∈
ℝ) |
26 | | ressxr 10407 |
. . . . . . . . . . . . 13
⊢ ℝ
⊆ ℝ* |
27 | | sseqin2 4046 |
. . . . . . . . . . . . 13
⊢ (ℝ
⊆ ℝ* ↔ (ℝ* ∩ ℝ) =
ℝ) |
28 | 26, 27 | mpbi 222 |
. . . . . . . . . . . 12
⊢
(ℝ* ∩ ℝ) = ℝ |
29 | 25, 28 | syl6eleqr 2917 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → 𝑦 ∈ (ℝ*
∩ ℝ)) |
30 | | rpxr 12130 |
. . . . . . . . . . . 12
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ*) |
31 | 30 | adantl 475 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈
ℝ*) |
32 | 22 | xrsdsre 22990 |
. . . . . . . . . . . . 13
⊢ (𝐷 ↾ (ℝ ×
ℝ)) = ((abs ∘ − ) ↾ (ℝ ×
ℝ)) |
33 | 32 | eqcomi 2834 |
. . . . . . . . . . . 12
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) = (𝐷 ↾ (ℝ ×
ℝ)) |
34 | 33 | blres 22613 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈
(∞Met‘ℝ*) ∧ 𝑦 ∈ (ℝ* ∩ ℝ)
∧ 𝑟 ∈
ℝ*) → (𝑦(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) = ((𝑦(ball‘𝐷)𝑟) ∩ ℝ)) |
35 | 24, 29, 31, 34 | syl3anc 1494 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → (𝑦(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) = ((𝑦(ball‘𝐷)𝑟) ∩ ℝ)) |
36 | 22 | xrsblre 22991 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℝ ∧ 𝑟 ∈ ℝ*)
→ (𝑦(ball‘𝐷)𝑟) ⊆ ℝ) |
37 | 30, 36 | sylan2 586 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℝ ∧ 𝑟 ∈ ℝ+)
→ (𝑦(ball‘𝐷)𝑟) ⊆ ℝ) |
38 | 37 | adantll 705 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → (𝑦(ball‘𝐷)𝑟) ⊆ ℝ) |
39 | | df-ss 3812 |
. . . . . . . . . . 11
⊢ ((𝑦(ball‘𝐷)𝑟) ⊆ ℝ ↔ ((𝑦(ball‘𝐷)𝑟) ∩ ℝ) = (𝑦(ball‘𝐷)𝑟)) |
40 | 38, 39 | sylib 210 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → ((𝑦(ball‘𝐷)𝑟) ∩ ℝ) = (𝑦(ball‘𝐷)𝑟)) |
41 | 35, 40 | eqtrd 2861 |
. . . . . . . . 9
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → (𝑦(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) = (𝑦(ball‘𝐷)𝑟)) |
42 | 41 | sseq1d 3857 |
. . . . . . . 8
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → ((𝑦(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑥 ∩ ℝ) ↔ (𝑦(ball‘𝐷)𝑟) ⊆ (𝑥 ∩ ℝ))) |
43 | | inss1 4059 |
. . . . . . . . 9
⊢ (𝑥 ∩ ℝ) ⊆ 𝑥 |
44 | | sstr 3835 |
. . . . . . . . 9
⊢ (((𝑦(ball‘𝐷)𝑟) ⊆ (𝑥 ∩ ℝ) ∧ (𝑥 ∩ ℝ) ⊆ 𝑥) → (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥) |
45 | 43, 44 | mpan2 682 |
. . . . . . . 8
⊢ ((𝑦(ball‘𝐷)𝑟) ⊆ (𝑥 ∩ ℝ) → (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥) |
46 | 42, 45 | syl6bi 245 |
. . . . . . 7
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → ((𝑦(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑥 ∩ ℝ) → (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)) |
47 | 46 | reximdva 3225 |
. . . . . 6
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) → (∃𝑟 ∈ ℝ+
(𝑦(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑥 ∩ ℝ) → ∃𝑟 ∈ ℝ+
(𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)) |
48 | 21, 47 | mpd 15 |
. . . . 5
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) → ∃𝑟 ∈ ℝ+
(𝑦(ball‘𝐷)𝑟) ⊆ 𝑥) |
49 | | 1rp 12123 |
. . . . . 6
⊢ 1 ∈
ℝ+ |
50 | 23 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → 𝐷 ∈
(∞Met‘ℝ*)) |
51 | 3 | sselda 3827 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ ℝ*) |
52 | 51 | adantr 474 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ*) |
53 | | rpxr 12130 |
. . . . . . . . . 10
⊢ (1 ∈
ℝ+ → 1 ∈ ℝ*) |
54 | 49, 53 | mp1i 13 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → 1 ∈
ℝ*) |
55 | | elbl 22570 |
. . . . . . . . 9
⊢ ((𝐷 ∈
(∞Met‘ℝ*) ∧ 𝑦 ∈ ℝ* ∧ 1 ∈
ℝ*) → (𝑧 ∈ (𝑦(ball‘𝐷)1) ↔ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1))) |
56 | 50, 52, 54, 55 | syl3anc 1494 |
. . . . . . . 8
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → (𝑧 ∈ (𝑦(ball‘𝐷)1) ↔ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1))) |
57 | | simp2 1171 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) → ¬ 𝑦 ∈ ℝ) |
58 | 23 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → 𝐷 ∈
(∞Met‘ℝ*)) |
59 | 51 | 3ad2ant1 1167 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) → 𝑦 ∈ ℝ*) |
60 | 59 | adantr 474 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → 𝑦 ∈ ℝ*) |
61 | | simpl3l 1305 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → 𝑧 ∈ ℝ*) |
62 | | xmetcl 22513 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈
(∞Met‘ℝ*) ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ*)
→ (𝑦𝐷𝑧) ∈
ℝ*) |
63 | 58, 60, 61, 62 | syl3anc 1494 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → (𝑦𝐷𝑧) ∈
ℝ*) |
64 | | 1red 10364 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → 1 ∈ ℝ) |
65 | | xmetge0 22526 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈
(∞Met‘ℝ*) ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ*)
→ 0 ≤ (𝑦𝐷𝑧)) |
66 | 58, 60, 61, 65 | syl3anc 1494 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → 0 ≤ (𝑦𝐷𝑧)) |
67 | | simpl3r 1307 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → (𝑦𝐷𝑧) < 1) |
68 | 49, 53 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℝ* |
69 | | xrltle 12275 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦𝐷𝑧) ∈ ℝ* ∧ 1 ∈
ℝ*) → ((𝑦𝐷𝑧) < 1 → (𝑦𝐷𝑧) ≤ 1)) |
70 | 63, 68, 69 | sylancl 580 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → ((𝑦𝐷𝑧) < 1 → (𝑦𝐷𝑧) ≤ 1)) |
71 | 67, 70 | mpd 15 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → (𝑦𝐷𝑧) ≤ 1) |
72 | | xrrege0 12300 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑦𝐷𝑧) ∈ ℝ* ∧ 1 ∈
ℝ) ∧ (0 ≤ (𝑦𝐷𝑧) ∧ (𝑦𝐷𝑧) ≤ 1)) → (𝑦𝐷𝑧) ∈ ℝ) |
73 | 63, 64, 66, 71, 72 | syl22anc 872 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → (𝑦𝐷𝑧) ∈ ℝ) |
74 | | simpr 479 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → 𝑦 ≠ 𝑧) |
75 | 22 | xrsdsreclb 20160 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℝ*
∧ 𝑧 ∈
ℝ* ∧ 𝑦
≠ 𝑧) → ((𝑦𝐷𝑧) ∈ ℝ ↔ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ))) |
76 | 60, 61, 74, 75 | syl3anc 1494 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → ((𝑦𝐷𝑧) ∈ ℝ ↔ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ))) |
77 | 73, 76 | mpbid 224 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) |
78 | 77 | simpld 490 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → 𝑦 ∈ ℝ) |
79 | 78 | ex 403 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) → (𝑦 ≠ 𝑧 → 𝑦 ∈ ℝ)) |
80 | 79 | necon1bd 3017 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) → (¬ 𝑦 ∈ ℝ → 𝑦 = 𝑧)) |
81 | | simp1r 1259 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) → 𝑦 ∈ 𝑥) |
82 | | elequ1 2171 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → (𝑦 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥)) |
83 | 81, 82 | syl5ibcom 237 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) → (𝑦 = 𝑧 → 𝑧 ∈ 𝑥)) |
84 | 80, 83 | syld 47 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) → (¬ 𝑦 ∈ ℝ → 𝑧 ∈ 𝑥)) |
85 | 57, 84 | mpd 15 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1)) → 𝑧 ∈ 𝑥) |
86 | 85 | 3expia 1154 |
. . . . . . . 8
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → ((𝑧 ∈ ℝ* ∧ (𝑦𝐷𝑧) < 1) → 𝑧 ∈ 𝑥)) |
87 | 56, 86 | sylbid 232 |
. . . . . . 7
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → (𝑧 ∈ (𝑦(ball‘𝐷)1) → 𝑧 ∈ 𝑥)) |
88 | 87 | ssrdv 3833 |
. . . . . 6
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → (𝑦(ball‘𝐷)1) ⊆ 𝑥) |
89 | | oveq2 6918 |
. . . . . . . 8
⊢ (𝑟 = 1 → (𝑦(ball‘𝐷)𝑟) = (𝑦(ball‘𝐷)1)) |
90 | 89 | sseq1d 3857 |
. . . . . . 7
⊢ (𝑟 = 1 → ((𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ (𝑦(ball‘𝐷)1) ⊆ 𝑥)) |
91 | 90 | rspcev 3526 |
. . . . . 6
⊢ ((1
∈ ℝ+ ∧ (𝑦(ball‘𝐷)1) ⊆ 𝑥) → ∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥) |
92 | 49, 88, 91 | sylancr 581 |
. . . . 5
⊢ (((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → ∃𝑟 ∈ ℝ+
(𝑦(ball‘𝐷)𝑟) ⊆ 𝑥) |
93 | 48, 92 | pm2.61dan 847 |
. . . 4
⊢ ((𝑥 ∈ (ordTop‘ ≤ )
∧ 𝑦 ∈ 𝑥) → ∃𝑟 ∈ ℝ+
(𝑦(ball‘𝐷)𝑟) ⊆ 𝑥) |
94 | 93 | ralrimiva 3175 |
. . 3
⊢ (𝑥 ∈ (ordTop‘ ≤ )
→ ∀𝑦 ∈
𝑥 ∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥) |
95 | | xrsmopn.1 |
. . . . 5
⊢ 𝐽 = (MetOpen‘𝐷) |
96 | 95 | elmopn2 22627 |
. . . 4
⊢ (𝐷 ∈
(∞Met‘ℝ*) → (𝑥 ∈ 𝐽 ↔ (𝑥 ⊆ ℝ* ∧
∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥))) |
97 | 23, 96 | ax-mp 5 |
. . 3
⊢ (𝑥 ∈ 𝐽 ↔ (𝑥 ⊆ ℝ* ∧
∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)) |
98 | 3, 94, 97 | sylanbrc 578 |
. 2
⊢ (𝑥 ∈ (ordTop‘ ≤ )
→ 𝑥 ∈ 𝐽) |
99 | 98 | ssriv 3831 |
1
⊢
(ordTop‘ ≤ ) ⊆ 𝐽 |