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

Theorem tgioo 24311
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 24306 . . 3 𝐷 ∈ (∞Metβ€˜β„)
3 tgioo.2 . . . 4 𝐽 = (MetOpenβ€˜π·)
43mopnval 23943 . . 3 (𝐷 ∈ (∞Metβ€˜β„) β†’ 𝐽 = (topGenβ€˜ran (ballβ€˜π·)))
52, 4ax-mp 5 . 2 𝐽 = (topGenβ€˜ran (ballβ€˜π·))
61blssioo 24310 . . 3 ran (ballβ€˜π·) βŠ† ran (,)
7 elssuni 4941 . . . . . . 7 (𝑣 ∈ ran (,) β†’ 𝑣 βŠ† βˆͺ ran (,))
8 unirnioo 13425 . . . . . . 7 ℝ = βˆͺ ran (,)
97, 8sseqtrrdi 4033 . . . . . 6 (𝑣 ∈ ran (,) β†’ 𝑣 βŠ† ℝ)
10 retopbas 24276 . . . . . . . . . 10 ran (,) ∈ TopBases
1110a1i 11 . . . . . . . . 9 ((𝑣 ∈ ran (,) ∧ π‘₯ ∈ 𝑣) β†’ ran (,) ∈ TopBases)
12 simpl 483 . . . . . . . . 9 ((𝑣 ∈ ran (,) ∧ π‘₯ ∈ 𝑣) β†’ 𝑣 ∈ ran (,))
139sselda 3982 . . . . . . . . . 10 ((𝑣 ∈ ran (,) ∧ π‘₯ ∈ 𝑣) β†’ π‘₯ ∈ ℝ)
14 1re 11213 . . . . . . . . . . . 12 1 ∈ ℝ
151bl2ioo 24307 . . . . . . . . . . . 12 ((π‘₯ ∈ ℝ ∧ 1 ∈ ℝ) β†’ (π‘₯(ballβ€˜π·)1) = ((π‘₯ βˆ’ 1)(,)(π‘₯ + 1)))
1614, 15mpan2 689 . . . . . . . . . . 11 (π‘₯ ∈ ℝ β†’ (π‘₯(ballβ€˜π·)1) = ((π‘₯ βˆ’ 1)(,)(π‘₯ + 1)))
17 ioof 13423 . . . . . . . . . . . . 13 (,):(ℝ* Γ— ℝ*)βŸΆπ’« ℝ
18 ffn 6717 . . . . . . . . . . . . 13 ((,):(ℝ* Γ— ℝ*)βŸΆπ’« ℝ β†’ (,) Fn (ℝ* Γ— ℝ*))
1917, 18ax-mp 5 . . . . . . . . . . . 12 (,) Fn (ℝ* Γ— ℝ*)
20 peano2rem 11526 . . . . . . . . . . . . 13 (π‘₯ ∈ ℝ β†’ (π‘₯ βˆ’ 1) ∈ ℝ)
2120rexrd 11263 . . . . . . . . . . . 12 (π‘₯ ∈ ℝ β†’ (π‘₯ βˆ’ 1) ∈ ℝ*)
22 peano2re 11386 . . . . . . . . . . . . 13 (π‘₯ ∈ ℝ β†’ (π‘₯ + 1) ∈ ℝ)
2322rexrd 11263 . . . . . . . . . . . 12 (π‘₯ ∈ ℝ β†’ (π‘₯ + 1) ∈ ℝ*)
24 fnovrn 7581 . . . . . . . . . . . 12 (((,) Fn (ℝ* Γ— ℝ*) ∧ (π‘₯ βˆ’ 1) ∈ ℝ* ∧ (π‘₯ + 1) ∈ ℝ*) β†’ ((π‘₯ βˆ’ 1)(,)(π‘₯ + 1)) ∈ ran (,))
2519, 21, 23, 24mp3an2i 1466 . . . . . . . . . . 11 (π‘₯ ∈ ℝ β†’ ((π‘₯ βˆ’ 1)(,)(π‘₯ + 1)) ∈ ran (,))
2616, 25eqeltrd 2833 . . . . . . . . . 10 (π‘₯ ∈ ℝ β†’ (π‘₯(ballβ€˜π·)1) ∈ ran (,))
2713, 26syl 17 . . . . . . . . 9 ((𝑣 ∈ ran (,) ∧ π‘₯ ∈ 𝑣) β†’ (π‘₯(ballβ€˜π·)1) ∈ ran (,))
28 simpr 485 . . . . . . . . . 10 ((𝑣 ∈ ran (,) ∧ π‘₯ ∈ 𝑣) β†’ π‘₯ ∈ 𝑣)
29 1rp 12977 . . . . . . . . . . . 12 1 ∈ ℝ+
30 blcntr 23918 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Metβ€˜β„) ∧ π‘₯ ∈ ℝ ∧ 1 ∈ ℝ+) β†’ π‘₯ ∈ (π‘₯(ballβ€˜π·)1))
312, 29, 30mp3an13 1452 . . . . . . . . . . 11 (π‘₯ ∈ ℝ β†’ π‘₯ ∈ (π‘₯(ballβ€˜π·)1))
3213, 31syl 17 . . . . . . . . . 10 ((𝑣 ∈ ran (,) ∧ π‘₯ ∈ 𝑣) β†’ π‘₯ ∈ (π‘₯(ballβ€˜π·)1))
3328, 32elind 4194 . . . . . . . . 9 ((𝑣 ∈ ran (,) ∧ π‘₯ ∈ 𝑣) β†’ π‘₯ ∈ (𝑣 ∩ (π‘₯(ballβ€˜π·)1)))
34 basis2 22453 . . . . . . . . 9 (((ran (,) ∈ TopBases ∧ 𝑣 ∈ ran (,)) ∧ ((π‘₯(ballβ€˜π·)1) ∈ ran (,) ∧ π‘₯ ∈ (𝑣 ∩ (π‘₯(ballβ€˜π·)1)))) β†’ βˆƒπ‘§ ∈ ran (,)(π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))))
3511, 12, 27, 33, 34syl22anc 837 . . . . . . . 8 ((𝑣 ∈ ran (,) ∧ π‘₯ ∈ 𝑣) β†’ βˆƒπ‘§ ∈ ran (,)(π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))))
36 ovelrn 7582 . . . . . . . . . . 11 ((,) Fn (ℝ* Γ— ℝ*) β†’ (𝑧 ∈ ran (,) ↔ βˆƒπ‘Ž ∈ ℝ* βˆƒπ‘ ∈ ℝ* 𝑧 = (π‘Ž(,)𝑏)))
3719, 36ax-mp 5 . . . . . . . . . 10 (𝑧 ∈ ran (,) ↔ βˆƒπ‘Ž ∈ ℝ* βˆƒπ‘ ∈ ℝ* 𝑧 = (π‘Ž(,)𝑏))
38 eleq2 2822 . . . . . . . . . . . . . . 15 (𝑧 = (π‘Ž(,)𝑏) β†’ (π‘₯ ∈ 𝑧 ↔ π‘₯ ∈ (π‘Ž(,)𝑏)))
39 sseq1 4007 . . . . . . . . . . . . . . 15 (𝑧 = (π‘Ž(,)𝑏) β†’ (𝑧 βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1)) ↔ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))))
4038, 39anbi12d 631 . . . . . . . . . . . . . 14 (𝑧 = (π‘Ž(,)𝑏) β†’ ((π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) ↔ (π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1)))))
41 inss2 4229 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 ∩ (π‘₯(ballβ€˜π·)1)) βŠ† (π‘₯(ballβ€˜π·)1)
42 sstr 3990 . . . . . . . . . . . . . . . . . . . . . 22 (((π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1)) ∧ (𝑣 ∩ (π‘₯(ballβ€˜π·)1)) βŠ† (π‘₯(ballβ€˜π·)1)) β†’ (π‘Ž(,)𝑏) βŠ† (π‘₯(ballβ€˜π·)1))
4341, 42mpan2 689 . . . . . . . . . . . . . . . . . . . . 21 ((π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1)) β†’ (π‘Ž(,)𝑏) βŠ† (π‘₯(ballβ€˜π·)1))
4443adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ (π‘Ž(,)𝑏) βŠ† (π‘₯(ballβ€˜π·)1))
45 elioore 13353 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ ∈ (π‘Ž(,)𝑏) β†’ π‘₯ ∈ ℝ)
4645adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ π‘₯ ∈ ℝ)
4746, 16syl 17 . . . . . . . . . . . . . . . . . . . 20 ((π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ (π‘₯(ballβ€˜π·)1) = ((π‘₯ βˆ’ 1)(,)(π‘₯ + 1)))
4844, 47sseqtrd 4022 . . . . . . . . . . . . . . . . . . 19 ((π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ (π‘Ž(,)𝑏) βŠ† ((π‘₯ βˆ’ 1)(,)(π‘₯ + 1)))
49 dfss 3966 . . . . . . . . . . . . . . . . . . 19 ((π‘Ž(,)𝑏) βŠ† ((π‘₯ βˆ’ 1)(,)(π‘₯ + 1)) ↔ (π‘Ž(,)𝑏) = ((π‘Ž(,)𝑏) ∩ ((π‘₯ βˆ’ 1)(,)(π‘₯ + 1))))
5048, 49sylib 217 . . . . . . . . . . . . . . . . . 18 ((π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ (π‘Ž(,)𝑏) = ((π‘Ž(,)𝑏) ∩ ((π‘₯ βˆ’ 1)(,)(π‘₯ + 1))))
51 eliooxr 13381 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ (π‘Ž(,)𝑏) β†’ (π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
5221, 23jca 512 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ ∈ ℝ β†’ ((π‘₯ βˆ’ 1) ∈ ℝ* ∧ (π‘₯ + 1) ∈ ℝ*))
5345, 52syl 17 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ (π‘Ž(,)𝑏) β†’ ((π‘₯ βˆ’ 1) ∈ ℝ* ∧ (π‘₯ + 1) ∈ ℝ*))
54 iooin 13357 . . . . . . . . . . . . . . . . . . . 20 (((π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*) ∧ ((π‘₯ βˆ’ 1) ∈ ℝ* ∧ (π‘₯ + 1) ∈ ℝ*)) β†’ ((π‘Ž(,)𝑏) ∩ ((π‘₯ βˆ’ 1)(,)(π‘₯ + 1))) = (if(π‘Ž ≀ (π‘₯ βˆ’ 1), (π‘₯ βˆ’ 1), π‘Ž)(,)if(𝑏 ≀ (π‘₯ + 1), 𝑏, (π‘₯ + 1))))
5551, 53, 54syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ (π‘Ž(,)𝑏) β†’ ((π‘Ž(,)𝑏) ∩ ((π‘₯ βˆ’ 1)(,)(π‘₯ + 1))) = (if(π‘Ž ≀ (π‘₯ βˆ’ 1), (π‘₯ βˆ’ 1), π‘Ž)(,)if(𝑏 ≀ (π‘₯ + 1), 𝑏, (π‘₯ + 1))))
5655adantr 481 . . . . . . . . . . . . . . . . . 18 ((π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ ((π‘Ž(,)𝑏) ∩ ((π‘₯ βˆ’ 1)(,)(π‘₯ + 1))) = (if(π‘Ž ≀ (π‘₯ βˆ’ 1), (π‘₯ βˆ’ 1), π‘Ž)(,)if(𝑏 ≀ (π‘₯ + 1), 𝑏, (π‘₯ + 1))))
5750, 56eqtrd 2772 . . . . . . . . . . . . . . . . 17 ((π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ (π‘Ž(,)𝑏) = (if(π‘Ž ≀ (π‘₯ βˆ’ 1), (π‘₯ βˆ’ 1), π‘Ž)(,)if(𝑏 ≀ (π‘₯ + 1), 𝑏, (π‘₯ + 1))))
58 mnfxr 11270 . . . . . . . . . . . . . . . . . . . 20 -∞ ∈ ℝ*
5958a1i 11 . . . . . . . . . . . . . . . . . . 19 ((π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ -∞ ∈ ℝ*)
6046, 21syl 17 . . . . . . . . . . . . . . . . . . . 20 ((π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ (π‘₯ βˆ’ 1) ∈ ℝ*)
6151adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ (π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
6261simpld 495 . . . . . . . . . . . . . . . . . . . 20 ((π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ π‘Ž ∈ ℝ*)
6360, 62ifcld 4574 . . . . . . . . . . . . . . . . . . 19 ((π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ if(π‘Ž ≀ (π‘₯ βˆ’ 1), (π‘₯ βˆ’ 1), π‘Ž) ∈ ℝ*)
6461simprd 496 . . . . . . . . . . . . . . . . . . . 20 ((π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ 𝑏 ∈ ℝ*)
6546, 22syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ (π‘₯ + 1) ∈ ℝ)
6665rexrd 11263 . . . . . . . . . . . . . . . . . . . 20 ((π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ (π‘₯ + 1) ∈ ℝ*)
6764, 66ifcld 4574 . . . . . . . . . . . . . . . . . . 19 ((π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ if(𝑏 ≀ (π‘₯ + 1), 𝑏, (π‘₯ + 1)) ∈ ℝ*)
6845, 20syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ ∈ (π‘Ž(,)𝑏) β†’ (π‘₯ βˆ’ 1) ∈ ℝ)
6968adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ (π‘₯ βˆ’ 1) ∈ ℝ)
7069mnfltd 13103 . . . . . . . . . . . . . . . . . . . 20 ((π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ -∞ < (π‘₯ βˆ’ 1))
71 xrmax2 13154 . . . . . . . . . . . . . . . . . . . . 21 ((π‘Ž ∈ ℝ* ∧ (π‘₯ βˆ’ 1) ∈ ℝ*) β†’ (π‘₯ βˆ’ 1) ≀ if(π‘Ž ≀ (π‘₯ βˆ’ 1), (π‘₯ βˆ’ 1), π‘Ž))
7262, 60, 71syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 ((π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ (π‘₯ βˆ’ 1) ≀ if(π‘Ž ≀ (π‘₯ βˆ’ 1), (π‘₯ βˆ’ 1), π‘Ž))
7359, 60, 63, 70, 72xrltletrd 13139 . . . . . . . . . . . . . . . . . . 19 ((π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ -∞ < if(π‘Ž ≀ (π‘₯ βˆ’ 1), (π‘₯ βˆ’ 1), π‘Ž))
74 simpl 483 . . . . . . . . . . . . . . . . . . . . 21 ((π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ π‘₯ ∈ (π‘Ž(,)𝑏))
7574, 57eleqtrd 2835 . . . . . . . . . . . . . . . . . . . 20 ((π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ π‘₯ ∈ (if(π‘Ž ≀ (π‘₯ βˆ’ 1), (π‘₯ βˆ’ 1), π‘Ž)(,)if(𝑏 ≀ (π‘₯ + 1), 𝑏, (π‘₯ + 1))))
76 eliooxr 13381 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ ∈ (if(π‘Ž ≀ (π‘₯ βˆ’ 1), (π‘₯ βˆ’ 1), π‘Ž)(,)if(𝑏 ≀ (π‘₯ + 1), 𝑏, (π‘₯ + 1))) β†’ (if(π‘Ž ≀ (π‘₯ βˆ’ 1), (π‘₯ βˆ’ 1), π‘Ž) ∈ ℝ* ∧ if(𝑏 ≀ (π‘₯ + 1), 𝑏, (π‘₯ + 1)) ∈ ℝ*))
77 ne0i 4334 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ ∈ (if(π‘Ž ≀ (π‘₯ βˆ’ 1), (π‘₯ βˆ’ 1), π‘Ž)(,)if(𝑏 ≀ (π‘₯ + 1), 𝑏, (π‘₯ + 1))) β†’ (if(π‘Ž ≀ (π‘₯ βˆ’ 1), (π‘₯ βˆ’ 1), π‘Ž)(,)if(𝑏 ≀ (π‘₯ + 1), 𝑏, (π‘₯ + 1))) β‰  βˆ…)
78 ioon0 13349 . . . . . . . . . . . . . . . . . . . . . 22 ((if(π‘Ž ≀ (π‘₯ βˆ’ 1), (π‘₯ βˆ’ 1), π‘Ž) ∈ ℝ* ∧ if(𝑏 ≀ (π‘₯ + 1), 𝑏, (π‘₯ + 1)) ∈ ℝ*) β†’ ((if(π‘Ž ≀ (π‘₯ βˆ’ 1), (π‘₯ βˆ’ 1), π‘Ž)(,)if(𝑏 ≀ (π‘₯ + 1), 𝑏, (π‘₯ + 1))) β‰  βˆ… ↔ if(π‘Ž ≀ (π‘₯ βˆ’ 1), (π‘₯ βˆ’ 1), π‘Ž) < if(𝑏 ≀ (π‘₯ + 1), 𝑏, (π‘₯ + 1))))
7977, 78imbitrid 243 . . . . . . . . . . . . . . . . . . . . 21 ((if(π‘Ž ≀ (π‘₯ βˆ’ 1), (π‘₯ βˆ’ 1), π‘Ž) ∈ ℝ* ∧ if(𝑏 ≀ (π‘₯ + 1), 𝑏, (π‘₯ + 1)) ∈ ℝ*) β†’ (π‘₯ ∈ (if(π‘Ž ≀ (π‘₯ βˆ’ 1), (π‘₯ βˆ’ 1), π‘Ž)(,)if(𝑏 ≀ (π‘₯ + 1), 𝑏, (π‘₯ + 1))) β†’ if(π‘Ž ≀ (π‘₯ βˆ’ 1), (π‘₯ βˆ’ 1), π‘Ž) < if(𝑏 ≀ (π‘₯ + 1), 𝑏, (π‘₯ + 1))))
8076, 79mpcom 38 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ (if(π‘Ž ≀ (π‘₯ βˆ’ 1), (π‘₯ βˆ’ 1), π‘Ž)(,)if(𝑏 ≀ (π‘₯ + 1), 𝑏, (π‘₯ + 1))) β†’ if(π‘Ž ≀ (π‘₯ βˆ’ 1), (π‘₯ βˆ’ 1), π‘Ž) < if(𝑏 ≀ (π‘₯ + 1), 𝑏, (π‘₯ + 1)))
8175, 80syl 17 . . . . . . . . . . . . . . . . . . 19 ((π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ if(π‘Ž ≀ (π‘₯ βˆ’ 1), (π‘₯ βˆ’ 1), π‘Ž) < if(𝑏 ≀ (π‘₯ + 1), 𝑏, (π‘₯ + 1)))
82 xrre2 13148 . . . . . . . . . . . . . . . . . . 19 (((-∞ ∈ ℝ* ∧ if(π‘Ž ≀ (π‘₯ βˆ’ 1), (π‘₯ βˆ’ 1), π‘Ž) ∈ ℝ* ∧ if(𝑏 ≀ (π‘₯ + 1), 𝑏, (π‘₯ + 1)) ∈ ℝ*) ∧ (-∞ < if(π‘Ž ≀ (π‘₯ βˆ’ 1), (π‘₯ βˆ’ 1), π‘Ž) ∧ if(π‘Ž ≀ (π‘₯ βˆ’ 1), (π‘₯ βˆ’ 1), π‘Ž) < if(𝑏 ≀ (π‘₯ + 1), 𝑏, (π‘₯ + 1)))) β†’ if(π‘Ž ≀ (π‘₯ βˆ’ 1), (π‘₯ βˆ’ 1), π‘Ž) ∈ ℝ)
8359, 63, 67, 73, 81, 82syl32anc 1378 . . . . . . . . . . . . . . . . . 18 ((π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ if(π‘Ž ≀ (π‘₯ βˆ’ 1), (π‘₯ βˆ’ 1), π‘Ž) ∈ ℝ)
84 mnfle 13113 . . . . . . . . . . . . . . . . . . . . 21 (if(π‘Ž ≀ (π‘₯ βˆ’ 1), (π‘₯ βˆ’ 1), π‘Ž) ∈ ℝ* β†’ -∞ ≀ if(π‘Ž ≀ (π‘₯ βˆ’ 1), (π‘₯ βˆ’ 1), π‘Ž))
8563, 84syl 17 . . . . . . . . . . . . . . . . . . . 20 ((π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ -∞ ≀ if(π‘Ž ≀ (π‘₯ βˆ’ 1), (π‘₯ βˆ’ 1), π‘Ž))
8659, 63, 67, 85, 81xrlelttrd 13138 . . . . . . . . . . . . . . . . . . 19 ((π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ -∞ < if(𝑏 ≀ (π‘₯ + 1), 𝑏, (π‘₯ + 1)))
87 xrmin2 13156 . . . . . . . . . . . . . . . . . . . 20 ((𝑏 ∈ ℝ* ∧ (π‘₯ + 1) ∈ ℝ*) β†’ if(𝑏 ≀ (π‘₯ + 1), 𝑏, (π‘₯ + 1)) ≀ (π‘₯ + 1))
8864, 66, 87syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ if(𝑏 ≀ (π‘₯ + 1), 𝑏, (π‘₯ + 1)) ≀ (π‘₯ + 1))
89 xrre 13147 . . . . . . . . . . . . . . . . . . 19 (((if(𝑏 ≀ (π‘₯ + 1), 𝑏, (π‘₯ + 1)) ∈ ℝ* ∧ (π‘₯ + 1) ∈ ℝ) ∧ (-∞ < if(𝑏 ≀ (π‘₯ + 1), 𝑏, (π‘₯ + 1)) ∧ if(𝑏 ≀ (π‘₯ + 1), 𝑏, (π‘₯ + 1)) ≀ (π‘₯ + 1))) β†’ if(𝑏 ≀ (π‘₯ + 1), 𝑏, (π‘₯ + 1)) ∈ ℝ)
9067, 65, 86, 88, 89syl22anc 837 . . . . . . . . . . . . . . . . . 18 ((π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ if(𝑏 ≀ (π‘₯ + 1), 𝑏, (π‘₯ + 1)) ∈ ℝ)
911ioo2blex 24309 . . . . . . . . . . . . . . . . . 18 ((if(π‘Ž ≀ (π‘₯ βˆ’ 1), (π‘₯ βˆ’ 1), π‘Ž) ∈ ℝ ∧ if(𝑏 ≀ (π‘₯ + 1), 𝑏, (π‘₯ + 1)) ∈ ℝ) β†’ (if(π‘Ž ≀ (π‘₯ βˆ’ 1), (π‘₯ βˆ’ 1), π‘Ž)(,)if(𝑏 ≀ (π‘₯ + 1), 𝑏, (π‘₯ + 1))) ∈ ran (ballβ€˜π·))
9283, 90, 91syl2anc 584 . . . . . . . . . . . . . . . . 17 ((π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ (if(π‘Ž ≀ (π‘₯ βˆ’ 1), (π‘₯ βˆ’ 1), π‘Ž)(,)if(𝑏 ≀ (π‘₯ + 1), 𝑏, (π‘₯ + 1))) ∈ ran (ballβ€˜π·))
9357, 92eqeltrd 2833 . . . . . . . . . . . . . . . 16 ((π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ (π‘Ž(,)𝑏) ∈ ran (ballβ€˜π·))
94 inss1 4228 . . . . . . . . . . . . . . . . . 18 (𝑣 ∩ (π‘₯(ballβ€˜π·)1)) βŠ† 𝑣
95 sstr 3990 . . . . . . . . . . . . . . . . . 18 (((π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1)) ∧ (𝑣 ∩ (π‘₯(ballβ€˜π·)1)) βŠ† 𝑣) β†’ (π‘Ž(,)𝑏) βŠ† 𝑣)
9694, 95mpan2 689 . . . . . . . . . . . . . . . . 17 ((π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1)) β†’ (π‘Ž(,)𝑏) βŠ† 𝑣)
9796adantl 482 . . . . . . . . . . . . . . . 16 ((π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ (π‘Ž(,)𝑏) βŠ† 𝑣)
98 sseq1 4007 . . . . . . . . . . . . . . . . . 18 (𝑧 = (π‘Ž(,)𝑏) β†’ (𝑧 βŠ† 𝑣 ↔ (π‘Ž(,)𝑏) βŠ† 𝑣))
9938, 98anbi12d 631 . . . . . . . . . . . . . . . . 17 (𝑧 = (π‘Ž(,)𝑏) β†’ ((π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑣) ↔ (π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† 𝑣)))
10099rspcev 3612 . . . . . . . . . . . . . . . 16 (((π‘Ž(,)𝑏) ∈ ran (ballβ€˜π·) ∧ (π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† 𝑣)) β†’ βˆƒπ‘§ ∈ ran (ballβ€˜π·)(π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑣))
10193, 74, 97, 100syl12anc 835 . . . . . . . . . . . . . . 15 ((π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ βˆƒπ‘§ ∈ ran (ballβ€˜π·)(π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑣))
102 blssex 23932 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (∞Metβ€˜β„) ∧ π‘₯ ∈ ℝ) β†’ (βˆƒπ‘§ ∈ ran (ballβ€˜π·)(π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑣) ↔ βˆƒπ‘¦ ∈ ℝ+ (π‘₯(ballβ€˜π·)𝑦) βŠ† 𝑣))
1032, 46, 102sylancr 587 . . . . . . . . . . . . . . 15 ((π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ (βˆƒπ‘§ ∈ ran (ballβ€˜π·)(π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑣) ↔ βˆƒπ‘¦ ∈ ℝ+ (π‘₯(ballβ€˜π·)𝑦) βŠ† 𝑣))
104101, 103mpbid 231 . . . . . . . . . . . . . 14 ((π‘₯ ∈ (π‘Ž(,)𝑏) ∧ (π‘Ž(,)𝑏) βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ βˆƒπ‘¦ ∈ ℝ+ (π‘₯(ballβ€˜π·)𝑦) βŠ† 𝑣)
10540, 104syl6bi 252 . . . . . . . . . . . . 13 (𝑧 = (π‘Ž(,)𝑏) β†’ ((π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ βˆƒπ‘¦ ∈ ℝ+ (π‘₯(ballβ€˜π·)𝑦) βŠ† 𝑣))
106105a1i 11 . . . . . . . . . . . 12 ((π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*) β†’ (𝑧 = (π‘Ž(,)𝑏) β†’ ((π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ βˆƒπ‘¦ ∈ ℝ+ (π‘₯(ballβ€˜π·)𝑦) βŠ† 𝑣)))
107106rexlimivv 3199 . . . . . . . . . . 11 (βˆƒπ‘Ž ∈ ℝ* βˆƒπ‘ ∈ ℝ* 𝑧 = (π‘Ž(,)𝑏) β†’ ((π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ βˆƒπ‘¦ ∈ ℝ+ (π‘₯(ballβ€˜π·)𝑦) βŠ† 𝑣))
108107imp 407 . . . . . . . . . 10 ((βˆƒπ‘Ž ∈ ℝ* βˆƒπ‘ ∈ ℝ* 𝑧 = (π‘Ž(,)𝑏) ∧ (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1)))) β†’ βˆƒπ‘¦ ∈ ℝ+ (π‘₯(ballβ€˜π·)𝑦) βŠ† 𝑣)
10937, 108sylanb 581 . . . . . . . . 9 ((𝑧 ∈ ran (,) ∧ (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1)))) β†’ βˆƒπ‘¦ ∈ ℝ+ (π‘₯(ballβ€˜π·)𝑦) βŠ† 𝑣)
110109rexlimiva 3147 . . . . . . . 8 (βˆƒπ‘§ ∈ ran (,)(π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† (𝑣 ∩ (π‘₯(ballβ€˜π·)1))) β†’ βˆƒπ‘¦ ∈ ℝ+ (π‘₯(ballβ€˜π·)𝑦) βŠ† 𝑣)
11135, 110syl 17 . . . . . . 7 ((𝑣 ∈ ran (,) ∧ π‘₯ ∈ 𝑣) β†’ βˆƒπ‘¦ ∈ ℝ+ (π‘₯(ballβ€˜π·)𝑦) βŠ† 𝑣)
112111ralrimiva 3146 . . . . . 6 (𝑣 ∈ ran (,) β†’ βˆ€π‘₯ ∈ 𝑣 βˆƒπ‘¦ ∈ ℝ+ (π‘₯(ballβ€˜π·)𝑦) βŠ† 𝑣)
1133elmopn2 23950 . . . . . . 7 (𝐷 ∈ (∞Metβ€˜β„) β†’ (𝑣 ∈ 𝐽 ↔ (𝑣 βŠ† ℝ ∧ βˆ€π‘₯ ∈ 𝑣 βˆƒπ‘¦ ∈ ℝ+ (π‘₯(ballβ€˜π·)𝑦) βŠ† 𝑣)))
1142, 113ax-mp 5 . . . . . 6 (𝑣 ∈ 𝐽 ↔ (𝑣 βŠ† ℝ ∧ βˆ€π‘₯ ∈ 𝑣 βˆƒπ‘¦ ∈ ℝ+ (π‘₯(ballβ€˜π·)𝑦) βŠ† 𝑣))
1159, 112, 114sylanbrc 583 . . . . 5 (𝑣 ∈ ran (,) β†’ 𝑣 ∈ 𝐽)
116115ssriv 3986 . . . 4 ran (,) βŠ† 𝐽
117116, 5sseqtri 4018 . . 3 ran (,) βŠ† (topGenβ€˜ran (ballβ€˜π·))
118 2basgen 22492 . . 3 ((ran (ballβ€˜π·) βŠ† ran (,) ∧ ran (,) βŠ† (topGenβ€˜ran (ballβ€˜π·))) β†’ (topGenβ€˜ran (ballβ€˜π·)) = (topGenβ€˜ran (,)))
1196, 117, 118mp2an 690 . 2 (topGenβ€˜ran (ballβ€˜π·)) = (topGenβ€˜ran (,))
1205, 119eqtr2i 2761 1 (topGenβ€˜ran (,)) = 𝐽
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070   ∩ cin 3947   βŠ† wss 3948  βˆ…c0 4322  ifcif 4528  π’« cpw 4602  βˆͺ cuni 4908   class class class wbr 5148   Γ— cxp 5674  ran crn 5677   β†Ύ cres 5678   ∘ ccom 5680   Fn wfn 6538  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7408  β„cr 11108  1c1 11110   + caddc 11112  -∞cmnf 11245  β„*cxr 11246   < clt 11247   ≀ cle 11248   βˆ’ cmin 11443  β„+crp 12973  (,)cioo 13323  abscabs 15180  topGenctg 17382  βˆžMetcxmet 20928  ballcbl 20930  MetOpencmopn 20933  TopBasesctb 22447
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724  ax-cnex 11165  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-i2m1 11177  ax-1ne0 11178  ax-1rid 11179  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182  ax-pre-lttri 11183  ax-pre-lttrn 11184  ax-pre-ltadd 11185  ax-pre-mulgt0 11186  ax-pre-sup 11187
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7364  df-ov 7411  df-oprab 7412  df-mpo 7413  df-om 7855  df-1st 7974  df-2nd 7975  df-frecs 8265  df-wrecs 8296  df-recs 8370  df-rdg 8409  df-er 8702  df-map 8821  df-en 8939  df-dom 8940  df-sdom 8941  df-sup 9436  df-inf 9437  df-pnf 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253  df-sub 11445  df-neg 11446  df-div 11871  df-nn 12212  df-2 12274  df-3 12275  df-n0 12472  df-z 12558  df-uz 12822  df-q 12932  df-rp 12974  df-xneg 13091  df-xadd 13092  df-xmul 13093  df-ioo 13327  df-seq 13966  df-exp 14027  df-cj 15045  df-re 15046  df-im 15047  df-sqrt 15181  df-abs 15182  df-topgen 17388  df-psmet 20935  df-xmet 20936  df-met 20937  df-bl 20938  df-mopn 20939  df-bases 22448
This theorem is referenced by:  qdensere2  24312  rehaus  24314  resubmet  24317  tgioo2  24318  xrsmopn  24327  iccntr  24336  icccmplem3  24339  reconnlem2  24342  opnreen  24346  metdscn2  24372  evthicc  24975  opnmbllem  25117  dvlip2  25511  lhop  25532  dvcnvre  25535  nmcvcn  29943  opnrebl  35200  opnrebl2  35201  ptrecube  36483  poimirlem30  36513  opnmbllem0  36519  reheibor  36702
  Copyright terms: Public domain W3C validator