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 o. - ) |` ( RR X. RR ) )
Assertion blssioo 
|- ran ( ball ` D ) C_ ran (,)

Proof

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