MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tgioo Structured version   Visualization version   GIF version

Theorem tgioo 22968
Description: The topology generated by open intervals of reals is the same as the open sets of the standard metric space on the reals. (Contributed by NM, 7-May-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
Hypotheses
Ref Expression
remet.1 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))
tgioo.2 𝐽 = (MetOpen‘𝐷)
Assertion
Ref Expression
tgioo (topGen‘ran (,)) = 𝐽

Proof of Theorem tgioo
Dummy variables 𝑥 𝑦 𝑧 𝑎 𝑏 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 remet.1 . . . 4 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))
21rexmet 22963 . . 3 𝐷 ∈ (∞Met‘ℝ)
3 tgioo.2 . . . 4 𝐽 = (MetOpen‘𝐷)
43mopnval 22612 . . 3 (𝐷 ∈ (∞Met‘ℝ) → 𝐽 = (topGen‘ran (ball‘𝐷)))
52, 4ax-mp 5 . 2 𝐽 = (topGen‘ran (ball‘𝐷))
61blssioo 22967 . . 3 ran (ball‘𝐷) ⊆ ran (,)
7 elssuni 4688 . . . . . . 7 (𝑣 ∈ ran (,) → 𝑣 ran (,))
8 unirnioo 12561 . . . . . . 7 ℝ = ran (,)
97, 8syl6sseqr 3876 . . . . . 6 (𝑣 ∈ ran (,) → 𝑣 ⊆ ℝ)
10 retopbas 22933 . . . . . . . . . 10 ran (,) ∈ TopBases
1110a1i 11 . . . . . . . . 9 ((𝑣 ∈ ran (,) ∧ 𝑥𝑣) → ran (,) ∈ TopBases)
12 simpl 476 . . . . . . . . 9 ((𝑣 ∈ ran (,) ∧ 𝑥𝑣) → 𝑣 ∈ ran (,))
139sselda 3826 . . . . . . . . . 10 ((𝑣 ∈ ran (,) ∧ 𝑥𝑣) → 𝑥 ∈ ℝ)
14 1re 10355 . . . . . . . . . . . 12 1 ∈ ℝ
151bl2ioo 22964 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 1 ∈ ℝ) → (𝑥(ball‘𝐷)1) = ((𝑥 − 1)(,)(𝑥 + 1)))
1614, 15mpan2 684 . . . . . . . . . . 11 (𝑥 ∈ ℝ → (𝑥(ball‘𝐷)1) = ((𝑥 − 1)(,)(𝑥 + 1)))
17 peano2rem 10668 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → (𝑥 − 1) ∈ ℝ)
1817rexrd 10405 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (𝑥 − 1) ∈ ℝ*)
19 peano2re 10527 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → (𝑥 + 1) ∈ ℝ)
2019rexrd 10405 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (𝑥 + 1) ∈ ℝ*)
21 ioof 12559 . . . . . . . . . . . . . 14 (,):(ℝ* × ℝ*)⟶𝒫 ℝ
22 ffn 6277 . . . . . . . . . . . . . 14 ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → (,) Fn (ℝ* × ℝ*))
2321, 22ax-mp 5 . . . . . . . . . . . . 13 (,) Fn (ℝ* × ℝ*)
24 fnovrn 7068 . . . . . . . . . . . . 13 (((,) Fn (ℝ* × ℝ*) ∧ (𝑥 − 1) ∈ ℝ* ∧ (𝑥 + 1) ∈ ℝ*) → ((𝑥 − 1)(,)(𝑥 + 1)) ∈ ran (,))
2523, 24mp3an1 1578 . . . . . . . . . . . 12 (((𝑥 − 1) ∈ ℝ* ∧ (𝑥 + 1) ∈ ℝ*) → ((𝑥 − 1)(,)(𝑥 + 1)) ∈ ran (,))
2618, 20, 25syl2anc 581 . . . . . . . . . . 11 (𝑥 ∈ ℝ → ((𝑥 − 1)(,)(𝑥 + 1)) ∈ ran (,))
2716, 26eqeltrd 2905 . . . . . . . . . 10 (𝑥 ∈ ℝ → (𝑥(ball‘𝐷)1) ∈ ran (,))
2813, 27syl 17 . . . . . . . . 9 ((𝑣 ∈ ran (,) ∧ 𝑥𝑣) → (𝑥(ball‘𝐷)1) ∈ ran (,))
29 simpr 479 . . . . . . . . . 10 ((𝑣 ∈ ran (,) ∧ 𝑥𝑣) → 𝑥𝑣)
30 1rp 12115 . . . . . . . . . . . 12 1 ∈ ℝ+
31 blcntr 22587 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Met‘ℝ) ∧ 𝑥 ∈ ℝ ∧ 1 ∈ ℝ+) → 𝑥 ∈ (𝑥(ball‘𝐷)1))
322, 30, 31mp3an13 1582 . . . . . . . . . . 11 (𝑥 ∈ ℝ → 𝑥 ∈ (𝑥(ball‘𝐷)1))
3313, 32syl 17 . . . . . . . . . 10 ((𝑣 ∈ ran (,) ∧ 𝑥𝑣) → 𝑥 ∈ (𝑥(ball‘𝐷)1))
3429, 33elind 4024 . . . . . . . . 9 ((𝑣 ∈ ran (,) ∧ 𝑥𝑣) → 𝑥 ∈ (𝑣 ∩ (𝑥(ball‘𝐷)1)))
35 basis2 21125 . . . . . . . . 9 (((ran (,) ∈ TopBases ∧ 𝑣 ∈ ran (,)) ∧ ((𝑥(ball‘𝐷)1) ∈ ran (,) ∧ 𝑥 ∈ (𝑣 ∩ (𝑥(ball‘𝐷)1)))) → ∃𝑧 ∈ ran (,)(𝑥𝑧𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))))
3611, 12, 28, 34, 35syl22anc 874 . . . . . . . 8 ((𝑣 ∈ ran (,) ∧ 𝑥𝑣) → ∃𝑧 ∈ ran (,)(𝑥𝑧𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))))
37 ovelrn 7069 . . . . . . . . . . 11 ((,) Fn (ℝ* × ℝ*) → (𝑧 ∈ ran (,) ↔ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* 𝑧 = (𝑎(,)𝑏)))
3823, 37ax-mp 5 . . . . . . . . . 10 (𝑧 ∈ ran (,) ↔ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* 𝑧 = (𝑎(,)𝑏))
39 eleq2 2894 . . . . . . . . . . . . . . 15 (𝑧 = (𝑎(,)𝑏) → (𝑥𝑧𝑥 ∈ (𝑎(,)𝑏)))
40 sseq1 3850 . . . . . . . . . . . . . . 15 (𝑧 = (𝑎(,)𝑏) → (𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ↔ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))))
4139, 40anbi12d 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))
4442, 43mpan2 684 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) → (𝑎(,)𝑏) ⊆ (𝑥(ball‘𝐷)1))
4544adantl 475 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) ⊆ (𝑥(ball‘𝐷)1))
46 elioore 12492 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝑎(,)𝑏) → 𝑥 ∈ ℝ)
4746adantr 474 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑥 ∈ ℝ)
4847, 16syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥(ball‘𝐷)1) = ((𝑥 − 1)(,)(𝑥 + 1)))
4945, 48sseqtrd 3865 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) ⊆ ((𝑥 − 1)(,)(𝑥 + 1)))
50 dfss 3812 . . . . . . . . . . . . . . . . . . 19 ((𝑎(,)𝑏) ⊆ ((𝑥 − 1)(,)(𝑥 + 1)) ↔ (𝑎(,)𝑏) = ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1))))
5149, 50sylib 210 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) = ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1))))
52 eliooxr 12519 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝑎(,)𝑏) → (𝑎 ∈ ℝ*𝑏 ∈ ℝ*))
5318, 20jca 509 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ → ((𝑥 − 1) ∈ ℝ* ∧ (𝑥 + 1) ∈ ℝ*))
5446, 53syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝑎(,)𝑏) → ((𝑥 − 1) ∈ ℝ* ∧ (𝑥 + 1) ∈ ℝ*))
55 iooin 12496 . . . . . . . . . . . . . . . . . . . 20 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑥 − 1) ∈ ℝ* ∧ (𝑥 + 1) ∈ ℝ*)) → ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1))) = (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))))
5652, 54, 55syl2anc 581 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1))) = (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))))
5756adantr 474 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1))) = (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))))
5851, 57eqtrd 2860 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) = (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))))
59 mnfxr 10413 . . . . . . . . . . . . . . . . . . . 20 -∞ ∈ ℝ*
6059a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ ∈ ℝ*)
6147, 18syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 − 1) ∈ ℝ*)
6252adantr 474 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎 ∈ ℝ*𝑏 ∈ ℝ*))
6362simpld 490 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑎 ∈ ℝ*)
6461, 63ifcld 4350 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ*)
6562simprd 491 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑏 ∈ ℝ*)
6647, 19syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 + 1) ∈ ℝ)
6766rexrd 10405 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 + 1) ∈ ℝ*)
6865, 67ifcld 4350 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ*)
6946, 17syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝑎(,)𝑏) → (𝑥 − 1) ∈ ℝ)
7069adantr 474 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 − 1) ∈ ℝ)
71 mnflt 12242 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 − 1) ∈ ℝ → -∞ < (𝑥 − 1))
7270, 71syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ < (𝑥 − 1))
73 xrmax2 12294 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎 ∈ ℝ* ∧ (𝑥 − 1) ∈ ℝ*) → (𝑥 − 1) ≤ if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎))
7463, 61, 73syl2anc 581 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 − 1) ≤ if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎))
7560, 61, 64, 72, 74xrltletrd 12279 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ < if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎))
76 simpl 476 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑥 ∈ (𝑎(,)𝑏))
7776, 58eleqtrd 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))))
8179, 80syl5ib 236 . . . . . . . . . . . . . . . . . . . . 21 ((if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ* ∧ if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ*) → (𝑥 ∈ (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) → if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) < if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))))
8278, 81mpcom 38 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) → if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) < if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)))
8377, 82syl 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), 𝑎) ∈ ℝ)
8560, 64, 68, 75, 83, 84syl32anc 1503 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ)
86 mnfle 12254 . . . . . . . . . . . . . . . . . . . . 21 (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ* → -∞ ≤ if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎))
8764, 86syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ ≤ if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎))
8860, 64, 68, 87, 83xrlelttrd 12278 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ < if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)))
89 xrmin2 12296 . . . . . . . . . . . . . . . . . . . 20 ((𝑏 ∈ ℝ* ∧ (𝑥 + 1) ∈ ℝ*) → if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ≤ (𝑥 + 1))
9065, 67, 89syl2anc 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)) ∈ ℝ)
9268, 66, 88, 90, 91syl22anc 874 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ)
931ioo2blex 22966 . . . . . . . . . . . . . . . . . 18 ((if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ ∧ if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ) → (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) ∈ ran (ball‘𝐷))
9485, 92, 93syl2anc 581 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) ∈ ran (ball‘𝐷))
9558, 94eqeltrd 2905 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) ∈ ran (ball‘𝐷))
96 inss1 4056 . . . . . . . . . . . . . . . . . 18 (𝑣 ∩ (𝑥(ball‘𝐷)1)) ⊆ 𝑣
97 sstr 3834 . . . . . . . . . . . . . . . . . 18 (((𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ∧ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ⊆ 𝑣) → (𝑎(,)𝑏) ⊆ 𝑣)
9896, 97mpan2 684 . . . . . . . . . . . . . . . . 17 ((𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) → (𝑎(,)𝑏) ⊆ 𝑣)
9998adantl 475 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) ⊆ 𝑣)
100 sseq1 3850 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑎(,)𝑏) → (𝑧𝑣 ↔ (𝑎(,)𝑏) ⊆ 𝑣))
10139, 100anbi12d 626 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑎(,)𝑏) → ((𝑥𝑧𝑧𝑣) ↔ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣)))
102101rspcev 3525 . . . . . . . . . . . . . . . 16 (((𝑎(,)𝑏) ∈ ran (ball‘𝐷) ∧ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣)) → ∃𝑧 ∈ ran (ball‘𝐷)(𝑥𝑧𝑧𝑣))
10395, 76, 99, 102syl12anc 872 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑧 ∈ ran (ball‘𝐷)(𝑥𝑧𝑧𝑣))
104 blssex 22601 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (∞Met‘ℝ) ∧ 𝑥 ∈ ℝ) → (∃𝑧 ∈ ran (ball‘𝐷)(𝑥𝑧𝑧𝑣) ↔ ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣))
1052, 47, 104sylancr 583 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (∃𝑧 ∈ ran (ball‘𝐷)(𝑥𝑧𝑧𝑣) ↔ ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣))
106103, 105mpbid 224 . . . . . . . . . . . . . 14 ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)
10741, 106syl6bi 245 . . . . . . . . . . . . 13 (𝑧 = (𝑎(,)𝑏) → ((𝑥𝑧𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣))
108107a1i 11 . . . . . . . . . . . 12 ((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) → (𝑧 = (𝑎(,)𝑏) → ((𝑥𝑧𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)))
109108rexlimivv 3245 . . . . . . . . . . 11 (∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* 𝑧 = (𝑎(,)𝑏) → ((𝑥𝑧𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣))
110109imp 397 . . . . . . . . . 10 ((∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* 𝑧 = (𝑎(,)𝑏) ∧ (𝑥𝑧𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)))) → ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)
11138, 110sylanb 578 . . . . . . . . 9 ((𝑧 ∈ ran (,) ∧ (𝑥𝑧𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)))) → ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)
112111rexlimiva 3236 . . . . . . . 8 (∃𝑧 ∈ ran (,)(𝑥𝑧𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)
11336, 112syl 17 . . . . . . 7 ((𝑣 ∈ ran (,) ∧ 𝑥𝑣) → ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)
114113ralrimiva 3174 . . . . . 6 (𝑣 ∈ ran (,) → ∀𝑥𝑣𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)
1153elmopn2 22619 . . . . . . 7 (𝐷 ∈ (∞Met‘ℝ) → (𝑣𝐽 ↔ (𝑣 ⊆ ℝ ∧ ∀𝑥𝑣𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)))
1162, 115ax-mp 5 . . . . . 6 (𝑣𝐽 ↔ (𝑣 ⊆ ℝ ∧ ∀𝑥𝑣𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣))
1179, 114, 116sylanbrc 580 . . . . 5 (𝑣 ∈ ran (,) → 𝑣𝐽)
118117ssriv 3830 . . . 4 ran (,) ⊆ 𝐽
119118, 5sseqtri 3861 . . 3 ran (,) ⊆ (topGen‘ran (ball‘𝐷))
120 2basgen 21164 . . 3 ((ran (ball‘𝐷) ⊆ ran (,) ∧ ran (,) ⊆ (topGen‘ran (ball‘𝐷))) → (topGen‘ran (ball‘𝐷)) = (topGen‘ran (,)))
1216, 119, 120mp2an 685 . 2 (topGen‘ran (ball‘𝐷)) = (topGen‘ran (,))
1225, 121eqtr2i 2849 1 (topGen‘ran (,)) = 𝐽
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386   = wceq 1658  wcel 2166  wne 2998  wral 3116  wrex 3117  cin 3796  wss 3797  c0 4143  ifcif 4305  𝒫 cpw 4377   cuni 4657   class class class wbr 4872   × cxp 5339  ran crn 5342  cres 5343  ccom 5345   Fn wfn 6117  wf 6118  cfv 6122  (class class class)co 6904  cr 10250  1c1 10252   + caddc 10254  -∞cmnf 10388  *cxr 10389   < clt 10390  cle 10391  cmin 10584  +crp 12111  (,)cioo 12462  abscabs 14350  topGenctg 16450  ∞Metcxmet 20090  ballcbl 20092  MetOpencmopn 20095  TopBasesctb 21119
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2390  ax-ext 2802  ax-sep 5004  ax-nul 5012  ax-pow 5064  ax-pr 5126  ax-un 7208  ax-cnex 10307  ax-resscn 10308  ax-1cn 10309  ax-icn 10310  ax-addcl 10311  ax-addrcl 10312  ax-mulcl 10313  ax-mulrcl 10314  ax-mulcom 10315  ax-addass 10316  ax-mulass 10317  ax-distr 10318  ax-i2m1 10319  ax-1ne0 10320  ax-1rid 10321  ax-rnegex 10322  ax-rrecex 10323  ax-cnre 10324  ax-pre-lttri 10325  ax-pre-lttrn 10326  ax-pre-ltadd 10327  ax-pre-mulgt0 10328  ax-pre-sup 10329
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2604  df-eu 2639  df-clab 2811  df-cleq 2817  df-clel 2820  df-nfc 2957  df-ne 2999  df-nel 3102  df-ral 3121  df-rex 3122  df-reu 3123  df-rmo 3124  df-rab 3125  df-v 3415  df-sbc 3662  df-csb 3757  df-dif 3800  df-un 3802  df-in 3804  df-ss 3811  df-pss 3813  df-nul 4144  df-if 4306  df-pw 4379  df-sn 4397  df-pr 4399  df-tp 4401  df-op 4403  df-uni 4658  df-iun 4741  df-br 4873  df-opab 4935  df-mpt 4952  df-tr 4975  df-id 5249  df-eprel 5254  df-po 5262  df-so 5263  df-fr 5300  df-we 5302  df-xp 5347  df-rel 5348  df-cnv 5349  df-co 5350  df-dm 5351  df-rn 5352  df-res 5353  df-ima 5354  df-pred 5919  df-ord 5965  df-on 5966  df-lim 5967  df-suc 5968  df-iota 6085  df-fun 6124  df-fn 6125  df-f 6126  df-f1 6127  df-fo 6128  df-f1o 6129  df-fv 6130  df-riota 6865  df-ov 6907  df-oprab 6908  df-mpt2 6909  df-om 7326  df-1st 7427  df-2nd 7428  df-wrecs 7671  df-recs 7733  df-rdg 7771  df-er 8008  df-map 8123  df-en 8222  df-dom 8223  df-sdom 8224  df-sup 8616  df-inf 8617  df-pnf 10392  df-mnf 10393  df-xr 10394  df-ltxr 10395  df-le 10396  df-sub 10586  df-neg 10587  df-div 11009  df-nn 11350  df-2 11413  df-3 11414  df-n0 11618  df-z 11704  df-uz 11968  df-q 12071  df-rp 12112  df-xneg 12231  df-xadd 12232  df-xmul 12233  df-ioo 12466  df-seq 13095  df-exp 13154  df-cj 14215  df-re 14216  df-im 14217  df-sqrt 14351  df-abs 14352  df-topgen 16456  df-psmet 20097  df-xmet 20098  df-met 20099  df-bl 20100  df-mopn 20101  df-bases 21120
This theorem is referenced by:  qdensere2  22969  rehaus  22971  resubmet  22974  tgioo2  22975  xrsmopn  22984  iccntr  22993  icccmplem3  22996  reconnlem2  22999  opnreen  23003  metdscn2  23029  evthicc  23624  opnmbllem  23766  dvlip2  24156  lhop  24177  dvcnvre  24180  nmcvcn  28104  opnrebl  32852  opnrebl2  32853  ptrecube  33952  poimirlem30  33982  opnmbllem0  33988  reheibor  34179
  Copyright terms: Public domain W3C validator