Step | Hyp | Ref
| Expression |
1 | | remet.1 |
. . . 4
⊢ 𝐷 = ((abs ∘ − )
↾ (ℝ × ℝ)) |
2 | 1 | rexmet 22963 |
. . 3
⊢ 𝐷 ∈
(∞Met‘ℝ) |
3 | | tgioo.2 |
. . . 4
⊢ 𝐽 = (MetOpen‘𝐷) |
4 | 3 | mopnval 22612 |
. . 3
⊢ (𝐷 ∈
(∞Met‘ℝ) → 𝐽 = (topGen‘ran (ball‘𝐷))) |
5 | 2, 4 | ax-mp 5 |
. 2
⊢ 𝐽 = (topGen‘ran
(ball‘𝐷)) |
6 | 1 | blssioo 22967 |
. . 3
⊢ ran
(ball‘𝐷) ⊆ ran
(,) |
7 | | elssuni 4688 |
. . . . . . 7
⊢ (𝑣 ∈ ran (,) → 𝑣 ⊆ ∪ ran (,)) |
8 | | unirnioo 12561 |
. . . . . . 7
⊢ ℝ =
∪ ran (,) |
9 | 7, 8 | syl6sseqr 3876 |
. . . . . 6
⊢ (𝑣 ∈ ran (,) → 𝑣 ⊆
ℝ) |
10 | | retopbas 22933 |
. . . . . . . . . 10
⊢ ran (,)
∈ TopBases |
11 | 10 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → ran (,) ∈
TopBases) |
12 | | simpl 476 |
. . . . . . . . 9
⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ ran (,)) |
13 | 9 | sselda 3826 |
. . . . . . . . . 10
⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ ℝ) |
14 | | 1re 10355 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ |
15 | 1 | bl2ioo 22964 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 1 ∈
ℝ) → (𝑥(ball‘𝐷)1) = ((𝑥 − 1)(,)(𝑥 + 1))) |
16 | 14, 15 | mpan2 684 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ → (𝑥(ball‘𝐷)1) = ((𝑥 − 1)(,)(𝑥 + 1))) |
17 | | peano2rem 10668 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ → (𝑥 − 1) ∈
ℝ) |
18 | 17 | rexrd 10405 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → (𝑥 − 1) ∈
ℝ*) |
19 | | peano2re 10527 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈
ℝ) |
20 | 19 | rexrd 10405 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈
ℝ*) |
21 | | ioof 12559 |
. . . . . . . . . . . . . 14
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
22 | | ffn 6277 |
. . . . . . . . . . . . . 14
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → (,) Fn (ℝ* ×
ℝ*)) |
23 | 21, 22 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (,) Fn
(ℝ* × ℝ*) |
24 | | fnovrn 7068 |
. . . . . . . . . . . . 13
⊢ (((,) Fn
(ℝ* × ℝ*) ∧ (𝑥 − 1) ∈ ℝ* ∧
(𝑥 + 1) ∈
ℝ*) → ((𝑥 − 1)(,)(𝑥 + 1)) ∈ ran (,)) |
25 | 23, 24 | mp3an1 1578 |
. . . . . . . . . . . 12
⊢ (((𝑥 − 1) ∈
ℝ* ∧ (𝑥 + 1) ∈ ℝ*) →
((𝑥 − 1)(,)(𝑥 + 1)) ∈ ran
(,)) |
26 | 18, 20, 25 | syl2anc 581 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ → ((𝑥 − 1)(,)(𝑥 + 1)) ∈ ran
(,)) |
27 | 16, 26 | eqeltrd 2905 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ → (𝑥(ball‘𝐷)1) ∈ ran (,)) |
28 | 13, 27 | syl 17 |
. . . . . . . . 9
⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → (𝑥(ball‘𝐷)1) ∈ ran (,)) |
29 | | simpr 479 |
. . . . . . . . . 10
⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ 𝑣) |
30 | | 1rp 12115 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ+ |
31 | | blcntr 22587 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈
(∞Met‘ℝ) ∧ 𝑥 ∈ ℝ ∧ 1 ∈
ℝ+) → 𝑥 ∈ (𝑥(ball‘𝐷)1)) |
32 | 2, 30, 31 | mp3an13 1582 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ → 𝑥 ∈ (𝑥(ball‘𝐷)1)) |
33 | 13, 32 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ (𝑥(ball‘𝐷)1)) |
34 | 29, 33 | elind 4024 |
. . . . . . . . 9
⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ (𝑣 ∩ (𝑥(ball‘𝐷)1))) |
35 | | basis2 21125 |
. . . . . . . . 9
⊢ (((ran
(,) ∈ TopBases ∧ 𝑣
∈ ran (,)) ∧ ((𝑥(ball‘𝐷)1) ∈ ran (,) ∧ 𝑥 ∈ (𝑣 ∩ (𝑥(ball‘𝐷)1)))) → ∃𝑧 ∈ ran (,)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)))) |
36 | 11, 12, 28, 34, 35 | syl22anc 874 |
. . . . . . . 8
⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → ∃𝑧 ∈ ran (,)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)))) |
37 | | ovelrn 7069 |
. . . . . . . . . . 11
⊢ ((,) Fn
(ℝ* × ℝ*) → (𝑧 ∈ ran (,) ↔ ∃𝑎 ∈ ℝ*
∃𝑏 ∈
ℝ* 𝑧 =
(𝑎(,)𝑏))) |
38 | 23, 37 | ax-mp 5 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ran (,) ↔
∃𝑎 ∈
ℝ* ∃𝑏 ∈ ℝ* 𝑧 = (𝑎(,)𝑏)) |
39 | | eleq2 2894 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑎(,)𝑏) → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ (𝑎(,)𝑏))) |
40 | | sseq1 3850 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑎(,)𝑏) → (𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ↔ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)))) |
41 | 39, 40 | anbi12d 626 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) ↔ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))))) |
42 | | inss2 4057 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ⊆ (𝑥(ball‘𝐷)1) |
43 | | sstr 3834 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ∧ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ⊆ (𝑥(ball‘𝐷)1)) → (𝑎(,)𝑏) ⊆ (𝑥(ball‘𝐷)1)) |
44 | 42, 43 | mpan2 684 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) → (𝑎(,)𝑏) ⊆ (𝑥(ball‘𝐷)1)) |
45 | 44 | adantl 475 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) ⊆ (𝑥(ball‘𝐷)1)) |
46 | | elioore 12492 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ (𝑎(,)𝑏) → 𝑥 ∈ ℝ) |
47 | 46 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑥 ∈ ℝ) |
48 | 47, 16 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥(ball‘𝐷)1) = ((𝑥 − 1)(,)(𝑥 + 1))) |
49 | 45, 48 | sseqtrd 3865 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) ⊆ ((𝑥 − 1)(,)(𝑥 + 1))) |
50 | | dfss 3812 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎(,)𝑏) ⊆ ((𝑥 − 1)(,)(𝑥 + 1)) ↔ (𝑎(,)𝑏) = ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1)))) |
51 | 49, 50 | sylib 210 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) = ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1)))) |
52 | | eliooxr 12519 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (𝑎(,)𝑏) → (𝑎 ∈ ℝ* ∧ 𝑏 ∈
ℝ*)) |
53 | 18, 20 | jca 509 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℝ → ((𝑥 − 1) ∈
ℝ* ∧ (𝑥 + 1) ∈
ℝ*)) |
54 | 46, 53 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (𝑎(,)𝑏) → ((𝑥 − 1) ∈ ℝ* ∧
(𝑥 + 1) ∈
ℝ*)) |
55 | | iooin 12496 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ ((𝑥 − 1) ∈ ℝ* ∧
(𝑥 + 1) ∈
ℝ*)) → ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1))) = (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)))) |
56 | 52, 54, 55 | syl2anc 581 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1))) = (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)))) |
57 | 56 | adantr 474 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1))) = (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)))) |
58 | 51, 57 | eqtrd 2860 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) = (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)))) |
59 | | mnfxr 10413 |
. . . . . . . . . . . . . . . . . . . 20
⊢ -∞
∈ ℝ* |
60 | 59 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ ∈
ℝ*) |
61 | 47, 18 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 − 1) ∈
ℝ*) |
62 | 52 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎 ∈ ℝ* ∧ 𝑏 ∈
ℝ*)) |
63 | 62 | simpld 490 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑎 ∈ ℝ*) |
64 | 61, 63 | ifcld 4350 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈
ℝ*) |
65 | 62 | simprd 491 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑏 ∈ ℝ*) |
66 | 47, 19 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 + 1) ∈ ℝ) |
67 | 66 | rexrd 10405 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 + 1) ∈
ℝ*) |
68 | 65, 67 | ifcld 4350 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈
ℝ*) |
69 | 46, 17 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ (𝑎(,)𝑏) → (𝑥 − 1) ∈ ℝ) |
70 | 69 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 − 1) ∈ ℝ) |
71 | | mnflt 12242 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 − 1) ∈ ℝ
→ -∞ < (𝑥
− 1)) |
72 | 70, 71 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ < (𝑥 − 1)) |
73 | | xrmax2 12294 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ∈ ℝ*
∧ (𝑥 − 1) ∈
ℝ*) → (𝑥 − 1) ≤ if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)) |
74 | 63, 61, 73 | syl2anc 581 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 − 1) ≤ if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)) |
75 | 60, 61, 64, 72, 74 | xrltletrd 12279 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ < if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)) |
76 | | simpl 476 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑥 ∈ (𝑎(,)𝑏)) |
77 | 76, 58 | eleqtrd 2907 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑥 ∈ (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)))) |
78 | | eliooxr 12519 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) → (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ* ∧ if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈
ℝ*)) |
79 | | ne0i 4149 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) → (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) ≠ ∅) |
80 | | ioon0 12488 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ* ∧ if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ*) →
((if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) ≠ ∅ ↔ if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) < if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)))) |
81 | 79, 80 | syl5ib 236 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ* ∧ if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ*) →
(𝑥 ∈ (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) → if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) < if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)))) |
82 | 78, 81 | mpcom 38 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) → if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) < if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) |
83 | 77, 82 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) < if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) |
84 | | xrre2 12288 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((-∞ ∈ ℝ* ∧ if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ* ∧ if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ*) ∧
(-∞ < if(𝑎 ≤
(𝑥 − 1), (𝑥 − 1), 𝑎) ∧ if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) < if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)))) → if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ) |
85 | 60, 64, 68, 75, 83, 84 | syl32anc 1503 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ) |
86 | | mnfle 12254 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ* → -∞
≤ if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)) |
87 | 64, 86 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ ≤ if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)) |
88 | 60, 64, 68, 87, 83 | xrlelttrd 12278 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ < if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) |
89 | | xrmin2 12296 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑏 ∈ ℝ*
∧ (𝑥 + 1) ∈
ℝ*) → if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ≤ (𝑥 + 1)) |
90 | 65, 67, 89 | syl2anc 581 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ≤ (𝑥 + 1)) |
91 | | xrre 12287 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ* ∧
(𝑥 + 1) ∈ ℝ)
∧ (-∞ < if(𝑏
≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∧ if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ≤ (𝑥 + 1))) → if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ) |
92 | 68, 66, 88, 90, 91 | syl22anc 874 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ) |
93 | 1 | ioo2blex 22966 |
. . . . . . . . . . . . . . . . . 18
⊢
((if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ ∧ if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ) → (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) ∈ ran (ball‘𝐷)) |
94 | 85, 92, 93 | syl2anc 581 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) ∈ ran (ball‘𝐷)) |
95 | 58, 94 | eqeltrd 2905 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) ∈ ran (ball‘𝐷)) |
96 | | inss1 4056 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ⊆ 𝑣 |
97 | | sstr 3834 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ∧ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ⊆ 𝑣) → (𝑎(,)𝑏) ⊆ 𝑣) |
98 | 96, 97 | mpan2 684 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) → (𝑎(,)𝑏) ⊆ 𝑣) |
99 | 98 | adantl 475 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) ⊆ 𝑣) |
100 | | sseq1 3850 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = (𝑎(,)𝑏) → (𝑧 ⊆ 𝑣 ↔ (𝑎(,)𝑏) ⊆ 𝑣)) |
101 | 39, 100 | anbi12d 626 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣) ↔ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣))) |
102 | 101 | rspcev 3525 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎(,)𝑏) ∈ ran (ball‘𝐷) ∧ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣)) → ∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣)) |
103 | 95, 76, 99, 102 | syl12anc 872 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣)) |
104 | | blssex 22601 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈
(∞Met‘ℝ) ∧ 𝑥 ∈ ℝ) → (∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣) ↔ ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)) |
105 | 2, 47, 104 | sylancr 583 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣) ↔ ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)) |
106 | 103, 105 | mpbid 224 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣) |
107 | 41, 106 | syl6bi 245 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)) |
108 | 107 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → (𝑧 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣))) |
109 | 108 | rexlimivv 3245 |
. . . . . . . . . . 11
⊢
(∃𝑎 ∈
ℝ* ∃𝑏 ∈ ℝ* 𝑧 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)) |
110 | 109 | imp 397 |
. . . . . . . . . 10
⊢
((∃𝑎 ∈
ℝ* ∃𝑏 ∈ ℝ* 𝑧 = (𝑎(,)𝑏) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)))) → ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣) |
111 | 38, 110 | sylanb 578 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ran (,) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)))) → ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣) |
112 | 111 | rexlimiva 3236 |
. . . . . . . 8
⊢
(∃𝑧 ∈ ran
(,)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣) |
113 | 36, 112 | syl 17 |
. . . . . . 7
⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣) |
114 | 113 | ralrimiva 3174 |
. . . . . 6
⊢ (𝑣 ∈ ran (,) →
∀𝑥 ∈ 𝑣 ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣) |
115 | 3 | elmopn2 22619 |
. . . . . . 7
⊢ (𝐷 ∈
(∞Met‘ℝ) → (𝑣 ∈ 𝐽 ↔ (𝑣 ⊆ ℝ ∧ ∀𝑥 ∈ 𝑣 ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣))) |
116 | 2, 115 | ax-mp 5 |
. . . . . 6
⊢ (𝑣 ∈ 𝐽 ↔ (𝑣 ⊆ ℝ ∧ ∀𝑥 ∈ 𝑣 ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)) |
117 | 9, 114, 116 | sylanbrc 580 |
. . . . 5
⊢ (𝑣 ∈ ran (,) → 𝑣 ∈ 𝐽) |
118 | 117 | ssriv 3830 |
. . . 4
⊢ ran (,)
⊆ 𝐽 |
119 | 118, 5 | sseqtri 3861 |
. . 3
⊢ ran (,)
⊆ (topGen‘ran (ball‘𝐷)) |
120 | | 2basgen 21164 |
. . 3
⊢ ((ran
(ball‘𝐷) ⊆ ran
(,) ∧ ran (,) ⊆ (topGen‘ran (ball‘𝐷))) → (topGen‘ran
(ball‘𝐷)) =
(topGen‘ran (,))) |
121 | 6, 119, 120 | mp2an 685 |
. 2
⊢
(topGen‘ran (ball‘𝐷)) = (topGen‘ran (,)) |
122 | 5, 121 | eqtr2i 2849 |
1
⊢
(topGen‘ran (,)) = 𝐽 |