| Step | Hyp | Ref
| Expression |
| 1 | | remet.1 |
. . . 4
⊢ 𝐷 = ((abs ∘ − )
↾ (ℝ × ℝ)) |
| 2 | 1 | rexmet 24812 |
. . 3
⊢ 𝐷 ∈
(∞Met‘ℝ) |
| 3 | | tgioo.2 |
. . . 4
⊢ 𝐽 = (MetOpen‘𝐷) |
| 4 | 3 | mopnval 24448 |
. . 3
⊢ (𝐷 ∈
(∞Met‘ℝ) → 𝐽 = (topGen‘ran (ball‘𝐷))) |
| 5 | 2, 4 | ax-mp 5 |
. 2
⊢ 𝐽 = (topGen‘ran
(ball‘𝐷)) |
| 6 | 1 | blssioo 24816 |
. . 3
⊢ ran
(ball‘𝐷) ⊆ ran
(,) |
| 7 | | elssuni 4937 |
. . . . . . 7
⊢ (𝑣 ∈ ran (,) → 𝑣 ⊆ ∪ ran (,)) |
| 8 | | unirnioo 13489 |
. . . . . . 7
⊢ ℝ =
∪ ran (,) |
| 9 | 7, 8 | sseqtrrdi 4025 |
. . . . . 6
⊢ (𝑣 ∈ ran (,) → 𝑣 ⊆
ℝ) |
| 10 | | retopbas 24781 |
. . . . . . . . . 10
⊢ ran (,)
∈ TopBases |
| 11 | 10 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → ran (,) ∈
TopBases) |
| 12 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ ran (,)) |
| 13 | 9 | sselda 3983 |
. . . . . . . . . 10
⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ ℝ) |
| 14 | | 1re 11261 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ |
| 15 | 1 | bl2ioo 24813 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 1 ∈
ℝ) → (𝑥(ball‘𝐷)1) = ((𝑥 − 1)(,)(𝑥 + 1))) |
| 16 | 14, 15 | mpan2 691 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ → (𝑥(ball‘𝐷)1) = ((𝑥 − 1)(,)(𝑥 + 1))) |
| 17 | | ioof 13487 |
. . . . . . . . . . . . 13
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
| 18 | | ffn 6736 |
. . . . . . . . . . . . 13
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → (,) Fn (ℝ* ×
ℝ*)) |
| 19 | 17, 18 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (,) Fn
(ℝ* × ℝ*) |
| 20 | | peano2rem 11576 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ → (𝑥 − 1) ∈
ℝ) |
| 21 | 20 | rexrd 11311 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → (𝑥 − 1) ∈
ℝ*) |
| 22 | | peano2re 11434 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈
ℝ) |
| 23 | 22 | rexrd 11311 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈
ℝ*) |
| 24 | | fnovrn 7608 |
. . . . . . . . . . . 12
⊢ (((,) Fn
(ℝ* × ℝ*) ∧ (𝑥 − 1) ∈ ℝ* ∧
(𝑥 + 1) ∈
ℝ*) → ((𝑥 − 1)(,)(𝑥 + 1)) ∈ ran (,)) |
| 25 | 19, 21, 23, 24 | mp3an2i 1468 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ → ((𝑥 − 1)(,)(𝑥 + 1)) ∈ ran
(,)) |
| 26 | 16, 25 | eqeltrd 2841 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ → (𝑥(ball‘𝐷)1) ∈ ran (,)) |
| 27 | 13, 26 | syl 17 |
. . . . . . . . 9
⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → (𝑥(ball‘𝐷)1) ∈ ran (,)) |
| 28 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ 𝑣) |
| 29 | | 1rp 13038 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ+ |
| 30 | | blcntr 24423 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈
(∞Met‘ℝ) ∧ 𝑥 ∈ ℝ ∧ 1 ∈
ℝ+) → 𝑥 ∈ (𝑥(ball‘𝐷)1)) |
| 31 | 2, 29, 30 | mp3an13 1454 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ → 𝑥 ∈ (𝑥(ball‘𝐷)1)) |
| 32 | 13, 31 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ (𝑥(ball‘𝐷)1)) |
| 33 | 28, 32 | elind 4200 |
. . . . . . . . 9
⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ (𝑣 ∩ (𝑥(ball‘𝐷)1))) |
| 34 | | basis2 22958 |
. . . . . . . . 9
⊢ (((ran
(,) ∈ TopBases ∧ 𝑣
∈ ran (,)) ∧ ((𝑥(ball‘𝐷)1) ∈ ran (,) ∧ 𝑥 ∈ (𝑣 ∩ (𝑥(ball‘𝐷)1)))) → ∃𝑧 ∈ ran (,)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)))) |
| 35 | 11, 12, 27, 33, 34 | syl22anc 839 |
. . . . . . . 8
⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → ∃𝑧 ∈ ran (,)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)))) |
| 36 | | ovelrn 7609 |
. . . . . . . . . . 11
⊢ ((,) Fn
(ℝ* × ℝ*) → (𝑧 ∈ ran (,) ↔ ∃𝑎 ∈ ℝ*
∃𝑏 ∈
ℝ* 𝑧 =
(𝑎(,)𝑏))) |
| 37 | 19, 36 | ax-mp 5 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ran (,) ↔
∃𝑎 ∈
ℝ* ∃𝑏 ∈ ℝ* 𝑧 = (𝑎(,)𝑏)) |
| 38 | | eleq2 2830 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑎(,)𝑏) → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ (𝑎(,)𝑏))) |
| 39 | | sseq1 4009 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑎(,)𝑏) → (𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ↔ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)))) |
| 40 | 38, 39 | anbi12d 632 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) ↔ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))))) |
| 41 | | inss2 4238 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ⊆ (𝑥(ball‘𝐷)1) |
| 42 | | sstr 3992 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ∧ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ⊆ (𝑥(ball‘𝐷)1)) → (𝑎(,)𝑏) ⊆ (𝑥(ball‘𝐷)1)) |
| 43 | 41, 42 | mpan2 691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) → (𝑎(,)𝑏) ⊆ (𝑥(ball‘𝐷)1)) |
| 44 | 43 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) ⊆ (𝑥(ball‘𝐷)1)) |
| 45 | | elioore 13417 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ (𝑎(,)𝑏) → 𝑥 ∈ ℝ) |
| 46 | 45 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑥 ∈ ℝ) |
| 47 | 46, 16 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥(ball‘𝐷)1) = ((𝑥 − 1)(,)(𝑥 + 1))) |
| 48 | 44, 47 | sseqtrd 4020 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) ⊆ ((𝑥 − 1)(,)(𝑥 + 1))) |
| 49 | | dfss 3970 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎(,)𝑏) ⊆ ((𝑥 − 1)(,)(𝑥 + 1)) ↔ (𝑎(,)𝑏) = ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1)))) |
| 50 | 48, 49 | sylib 218 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) = ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1)))) |
| 51 | | eliooxr 13445 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (𝑎(,)𝑏) → (𝑎 ∈ ℝ* ∧ 𝑏 ∈
ℝ*)) |
| 52 | 21, 23 | jca 511 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℝ → ((𝑥 − 1) ∈
ℝ* ∧ (𝑥 + 1) ∈
ℝ*)) |
| 53 | 45, 52 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (𝑎(,)𝑏) → ((𝑥 − 1) ∈ ℝ* ∧
(𝑥 + 1) ∈
ℝ*)) |
| 54 | | iooin 13421 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ ((𝑥 − 1) ∈ ℝ* ∧
(𝑥 + 1) ∈
ℝ*)) → ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1))) = (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)))) |
| 55 | 51, 53, 54 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1))) = (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)))) |
| 56 | 55 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1))) = (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)))) |
| 57 | 50, 56 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) = (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)))) |
| 58 | | mnfxr 11318 |
. . . . . . . . . . . . . . . . . . . 20
⊢ -∞
∈ ℝ* |
| 59 | 58 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ ∈
ℝ*) |
| 60 | 46, 21 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 − 1) ∈
ℝ*) |
| 61 | 51 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎 ∈ ℝ* ∧ 𝑏 ∈
ℝ*)) |
| 62 | 61 | simpld 494 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑎 ∈ ℝ*) |
| 63 | 60, 62 | ifcld 4572 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈
ℝ*) |
| 64 | 61 | simprd 495 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑏 ∈ ℝ*) |
| 65 | 46, 22 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 + 1) ∈ ℝ) |
| 66 | 65 | rexrd 11311 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 + 1) ∈
ℝ*) |
| 67 | 64, 66 | ifcld 4572 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈
ℝ*) |
| 68 | 45, 20 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ (𝑎(,)𝑏) → (𝑥 − 1) ∈ ℝ) |
| 69 | 68 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 − 1) ∈ ℝ) |
| 70 | 69 | mnfltd 13166 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ < (𝑥 − 1)) |
| 71 | | xrmax2 13218 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ∈ ℝ*
∧ (𝑥 − 1) ∈
ℝ*) → (𝑥 − 1) ≤ if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)) |
| 72 | 62, 60, 71 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 − 1) ≤ if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)) |
| 73 | 59, 60, 63, 70, 72 | xrltletrd 13203 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ < if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)) |
| 74 | | simpl 482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑥 ∈ (𝑎(,)𝑏)) |
| 75 | 74, 57 | eleqtrd 2843 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑥 ∈ (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)))) |
| 76 | | eliooxr 13445 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) → (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ* ∧ if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈
ℝ*)) |
| 77 | | ne0i 4341 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) → (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) ≠ ∅) |
| 78 | | ioon0 13413 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ* ∧ if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ*) →
((if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) ≠ ∅ ↔ if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) < if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)))) |
| 79 | 77, 78 | imbitrid 244 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ* ∧ if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ*) →
(𝑥 ∈ (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) → if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) < if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)))) |
| 80 | 76, 79 | mpcom 38 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) → if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) < if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) |
| 81 | 75, 80 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) < if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) |
| 82 | | xrre2 13212 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((-∞ ∈ ℝ* ∧ if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ* ∧ if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ*) ∧
(-∞ < if(𝑎 ≤
(𝑥 − 1), (𝑥 − 1), 𝑎) ∧ if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) < if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)))) → if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ) |
| 83 | 59, 63, 67, 73, 81, 82 | syl32anc 1380 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ) |
| 84 | | mnfle 13177 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ* → -∞
≤ if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)) |
| 85 | 63, 84 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ ≤ if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)) |
| 86 | 59, 63, 67, 85, 81 | xrlelttrd 13202 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ < if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) |
| 87 | | xrmin2 13220 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑏 ∈ ℝ*
∧ (𝑥 + 1) ∈
ℝ*) → if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ≤ (𝑥 + 1)) |
| 88 | 64, 66, 87 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ≤ (𝑥 + 1)) |
| 89 | | xrre 13211 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ* ∧
(𝑥 + 1) ∈ ℝ)
∧ (-∞ < if(𝑏
≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∧ if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ≤ (𝑥 + 1))) → if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ) |
| 90 | 67, 65, 86, 88, 89 | syl22anc 839 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ) |
| 91 | 1 | ioo2blex 24815 |
. . . . . . . . . . . . . . . . . 18
⊢
((if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ ∧ if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ) → (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) ∈ ran (ball‘𝐷)) |
| 92 | 83, 90, 91 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) ∈ ran (ball‘𝐷)) |
| 93 | 57, 92 | eqeltrd 2841 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) ∈ ran (ball‘𝐷)) |
| 94 | | inss1 4237 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ⊆ 𝑣 |
| 95 | | sstr 3992 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ∧ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ⊆ 𝑣) → (𝑎(,)𝑏) ⊆ 𝑣) |
| 96 | 94, 95 | mpan2 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) → (𝑎(,)𝑏) ⊆ 𝑣) |
| 97 | 96 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) ⊆ 𝑣) |
| 98 | | sseq1 4009 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = (𝑎(,)𝑏) → (𝑧 ⊆ 𝑣 ↔ (𝑎(,)𝑏) ⊆ 𝑣)) |
| 99 | 38, 98 | anbi12d 632 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣) ↔ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣))) |
| 100 | 99 | rspcev 3622 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎(,)𝑏) ∈ ran (ball‘𝐷) ∧ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣)) → ∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣)) |
| 101 | 93, 74, 97, 100 | syl12anc 837 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣)) |
| 102 | | blssex 24437 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈
(∞Met‘ℝ) ∧ 𝑥 ∈ ℝ) → (∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣) ↔ ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)) |
| 103 | 2, 46, 102 | sylancr 587 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣) ↔ ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)) |
| 104 | 101, 103 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣) |
| 105 | 40, 104 | biimtrdi 253 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)) |
| 106 | 105 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → (𝑧 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣))) |
| 107 | 106 | rexlimivv 3201 |
. . . . . . . . . . 11
⊢
(∃𝑎 ∈
ℝ* ∃𝑏 ∈ ℝ* 𝑧 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)) |
| 108 | 107 | imp 406 |
. . . . . . . . . 10
⊢
((∃𝑎 ∈
ℝ* ∃𝑏 ∈ ℝ* 𝑧 = (𝑎(,)𝑏) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)))) → ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣) |
| 109 | 37, 108 | sylanb 581 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ran (,) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)))) → ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣) |
| 110 | 109 | rexlimiva 3147 |
. . . . . . . 8
⊢
(∃𝑧 ∈ ran
(,)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣) |
| 111 | 35, 110 | syl 17 |
. . . . . . 7
⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣) |
| 112 | 111 | ralrimiva 3146 |
. . . . . 6
⊢ (𝑣 ∈ ran (,) →
∀𝑥 ∈ 𝑣 ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣) |
| 113 | 3 | elmopn2 24455 |
. . . . . . 7
⊢ (𝐷 ∈
(∞Met‘ℝ) → (𝑣 ∈ 𝐽 ↔ (𝑣 ⊆ ℝ ∧ ∀𝑥 ∈ 𝑣 ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣))) |
| 114 | 2, 113 | ax-mp 5 |
. . . . . 6
⊢ (𝑣 ∈ 𝐽 ↔ (𝑣 ⊆ ℝ ∧ ∀𝑥 ∈ 𝑣 ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)) |
| 115 | 9, 112, 114 | sylanbrc 583 |
. . . . 5
⊢ (𝑣 ∈ ran (,) → 𝑣 ∈ 𝐽) |
| 116 | 115 | ssriv 3987 |
. . . 4
⊢ ran (,)
⊆ 𝐽 |
| 117 | 116, 5 | sseqtri 4032 |
. . 3
⊢ ran (,)
⊆ (topGen‘ran (ball‘𝐷)) |
| 118 | | 2basgen 22997 |
. . 3
⊢ ((ran
(ball‘𝐷) ⊆ ran
(,) ∧ ran (,) ⊆ (topGen‘ran (ball‘𝐷))) → (topGen‘ran
(ball‘𝐷)) =
(topGen‘ran (,))) |
| 119 | 6, 117, 118 | mp2an 692 |
. 2
⊢
(topGen‘ran (ball‘𝐷)) = (topGen‘ran (,)) |
| 120 | 5, 119 | eqtr2i 2766 |
1
⊢
(topGen‘ran (,)) = 𝐽 |