Metamath Proof Explorer


Theorem blssioo

Description: The balls of the standard real metric space are included in the open real intervals. (Contributed by NM, 8-May-2007) (Revised by Mario Carneiro, 13-Nov-2013)

Ref Expression
Hypothesis remet.1 D = abs 2
Assertion blssioo ran ball D ran .

Proof

Step Hyp Ref Expression
1 remet.1 D = abs 2
2 1 rexmet D ∞Met
3 blrn D ∞Met z ran ball D y r * z = y ball D r
4 2 3 ax-mp z ran ball D y r * z = y ball D r
5 elxr r * r r = +∞ r = −∞
6 1 bl2ioo y r y ball D r = y r y + r
7 resubcl y r y r
8 readdcl y r y + r
9 ioof . : * × * 𝒫
10 ffn . : * × * 𝒫 . Fn * × *
11 9 10 ax-mp . Fn * × *
12 rexr y r y r *
13 rexr y + r y + r *
14 fnovrn . Fn * × * y r * y + r * y r y + r ran .
15 11 12 13 14 mp3an3an y r y + r y r y + r ran .
16 7 8 15 syl2anc y r y r y + r ran .
17 6 16 eqeltrd y r y ball D r ran .
18 oveq2 r = +∞ y ball D r = y ball D +∞
19 1 remet D Met
20 blpnf D Met y y ball D +∞ =
21 19 20 mpan y y ball D +∞ =
22 18 21 sylan9eqr y r = +∞ y ball D r =
23 ioomax −∞ +∞ =
24 ioorebas −∞ +∞ ran .
25 23 24 eqeltrri ran .
26 22 25 eqeltrdi y r = +∞ y ball D r ran .
27 oveq2 r = −∞ y ball D r = y ball D −∞
28 0xr 0 *
29 nltmnf 0 * ¬ 0 < −∞
30 28 29 ax-mp ¬ 0 < −∞
31 mnfxr −∞ *
32 xbln0 D ∞Met y −∞ * y ball D −∞ 0 < −∞
33 2 31 32 mp3an13 y y ball D −∞ 0 < −∞
34 33 necon1bbid y ¬ 0 < −∞ y ball D −∞ =
35 30 34 mpbii y y ball D −∞ =
36 27 35 sylan9eqr y r = −∞ y ball D r =
37 iooid 0 0 =
38 ioorebas 0 0 ran .
39 37 38 eqeltrri ran .
40 36 39 eqeltrdi y r = −∞ y ball D r ran .
41 17 26 40 3jaodan y r r = +∞ r = −∞ y ball D r ran .
42 5 41 sylan2b y r * y ball D r ran .
43 eleq1 z = y ball D r z ran . y ball D r ran .
44 42 43 syl5ibrcom y r * z = y ball D r z ran .
45 44 rexlimivv y r * z = y ball D r z ran .
46 4 45 sylbi z ran ball D z ran .
47 46 ssriv ran ball D ran .