Metamath Proof Explorer

Theorem opnrebl2

Description: A set is open in the standard topology of the reals precisely when every point can be enclosed in an arbitrarily small ball. (Contributed by Jeff Hankins, 22-Sep-2013) (Proof shortened by Mario Carneiro, 30-Jan-2014)

Ref Expression
Assertion opnrebl2 
|- ( A e. ( topGen ` ran (,) ) <-> ( A C_ RR /\ A. x e. A A. y e. RR+ E. z e. RR+ ( z <_ y /\ ( ( x - z ) (,) ( x + z ) ) C_ A ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) )
2 1 rexmet 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR )
3 eqid 
 |-  ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
4 1 3 tgioo 
 |-  ( topGen ` ran (,) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
5 4 mopnss 
 |-  ( ( ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR ) /\ A e. ( topGen ` ran (,) ) ) -> A C_ RR )
6 2 5 mpan 
 |-  ( A e. ( topGen ` ran (,) ) -> A C_ RR )
7 4 mopni3 
 |-  ( ( ( ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR ) /\ A e. ( topGen ` ran (,) ) /\ x e. A ) /\ y e. RR+ ) -> E. z e. RR+ ( z < y /\ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) z ) C_ A ) )
8 7 ex 
 |-  ( ( ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR ) /\ A e. ( topGen ` ran (,) ) /\ x e. A ) -> ( y e. RR+ -> E. z e. RR+ ( z < y /\ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) z ) C_ A ) ) )
9 2 8 mp3an1 
 |-  ( ( A e. ( topGen ` ran (,) ) /\ x e. A ) -> ( y e. RR+ -> E. z e. RR+ ( z < y /\ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) z ) C_ A ) ) )
10 6 sselda 
 |-  ( ( A e. ( topGen ` ran (,) ) /\ x e. A ) -> x e. RR )
11 rpre 
 |-  ( z e. RR+ -> z e. RR )
12 1 bl2ioo 
 |-  ( ( x e. RR /\ z e. RR ) -> ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) z ) = ( ( x - z ) (,) ( x + z ) ) )
13 11 12 sylan2 
 |-  ( ( x e. RR /\ z e. RR+ ) -> ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) z ) = ( ( x - z ) (,) ( x + z ) ) )
14 13 sseq1d 
 |-  ( ( x e. RR /\ z e. RR+ ) -> ( ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) z ) C_ A <-> ( ( x - z ) (,) ( x + z ) ) C_ A ) )
15 14 anbi2d 
 |-  ( ( x e. RR /\ z e. RR+ ) -> ( ( z < y /\ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) z ) C_ A ) <-> ( z < y /\ ( ( x - z ) (,) ( x + z ) ) C_ A ) ) )
16 15 rexbidva 
 |-  ( x e. RR -> ( E. z e. RR+ ( z < y /\ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) z ) C_ A ) <-> E. z e. RR+ ( z < y /\ ( ( x - z ) (,) ( x + z ) ) C_ A ) ) )
17 16 biimpd 
 |-  ( x e. RR -> ( E. z e. RR+ ( z < y /\ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) z ) C_ A ) -> E. z e. RR+ ( z < y /\ ( ( x - z ) (,) ( x + z ) ) C_ A ) ) )
18 rpre 
 |-  ( y e. RR+ -> y e. RR )
19 ltle 
 |-  ( ( z e. RR /\ y e. RR ) -> ( z < y -> z <_ y ) )
20 11 18 19 syl2anr 
 |-  ( ( y e. RR+ /\ z e. RR+ ) -> ( z < y -> z <_ y ) )
21 20 anim1d 
 |-  ( ( y e. RR+ /\ z e. RR+ ) -> ( ( z < y /\ ( ( x - z ) (,) ( x + z ) ) C_ A ) -> ( z <_ y /\ ( ( x - z ) (,) ( x + z ) ) C_ A ) ) )
22 21 reximdva 
 |-  ( y e. RR+ -> ( E. z e. RR+ ( z < y /\ ( ( x - z ) (,) ( x + z ) ) C_ A ) -> E. z e. RR+ ( z <_ y /\ ( ( x - z ) (,) ( x + z ) ) C_ A ) ) )
23 17 22 syl9 
 |-  ( x e. RR -> ( y e. RR+ -> ( E. z e. RR+ ( z < y /\ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) z ) C_ A ) -> E. z e. RR+ ( z <_ y /\ ( ( x - z ) (,) ( x + z ) ) C_ A ) ) ) )
24 10 23 syl 
 |-  ( ( A e. ( topGen ` ran (,) ) /\ x e. A ) -> ( y e. RR+ -> ( E. z e. RR+ ( z < y /\ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) z ) C_ A ) -> E. z e. RR+ ( z <_ y /\ ( ( x - z ) (,) ( x + z ) ) C_ A ) ) ) )
25 9 24 mpdd 
 |-  ( ( A e. ( topGen ` ran (,) ) /\ x e. A ) -> ( y e. RR+ -> E. z e. RR+ ( z <_ y /\ ( ( x - z ) (,) ( x + z ) ) C_ A ) ) )
26 25 expimpd 
 |-  ( A e. ( topGen ` ran (,) ) -> ( ( x e. A /\ y e. RR+ ) -> E. z e. RR+ ( z <_ y /\ ( ( x - z ) (,) ( x + z ) ) C_ A ) ) )
27 26 ralrimivv 
 |-  ( A e. ( topGen ` ran (,) ) -> A. x e. A A. y e. RR+ E. z e. RR+ ( z <_ y /\ ( ( x - z ) (,) ( x + z ) ) C_ A ) )
28 6 27 jca 
 |-  ( A e. ( topGen ` ran (,) ) -> ( A C_ RR /\ A. x e. A A. y e. RR+ E. z e. RR+ ( z <_ y /\ ( ( x - z ) (,) ( x + z ) ) C_ A ) ) )
29 ssel2 
 |-  ( ( A C_ RR /\ x e. A ) -> x e. RR )
30 1rp 
 |-  1 e. RR+
31 simpr 
 |-  ( ( z <_ y /\ ( ( x - z ) (,) ( x + z ) ) C_ A ) -> ( ( x - z ) (,) ( x + z ) ) C_ A )
32 31 reximi 
 |-  ( E. z e. RR+ ( z <_ y /\ ( ( x - z ) (,) ( x + z ) ) C_ A ) -> E. z e. RR+ ( ( x - z ) (,) ( x + z ) ) C_ A )
33 32 ralimi 
 |-  ( A. y e. RR+ E. z e. RR+ ( z <_ y /\ ( ( x - z ) (,) ( x + z ) ) C_ A ) -> A. y e. RR+ E. z e. RR+ ( ( x - z ) (,) ( x + z ) ) C_ A )
34 biidd 
 |-  ( y = 1 -> ( E. z e. RR+ ( ( x - z ) (,) ( x + z ) ) C_ A <-> E. z e. RR+ ( ( x - z ) (,) ( x + z ) ) C_ A ) )
35 34 rspcv 
 |-  ( 1 e. RR+ -> ( A. y e. RR+ E. z e. RR+ ( ( x - z ) (,) ( x + z ) ) C_ A -> E. z e. RR+ ( ( x - z ) (,) ( x + z ) ) C_ A ) )
36 30 33 35 mpsyl 
 |-  ( A. y e. RR+ E. z e. RR+ ( z <_ y /\ ( ( x - z ) (,) ( x + z ) ) C_ A ) -> E. z e. RR+ ( ( x - z ) (,) ( x + z ) ) C_ A )
37 14 rexbidva 
 |-  ( x e. RR -> ( E. z e. RR+ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) z ) C_ A <-> E. z e. RR+ ( ( x - z ) (,) ( x + z ) ) C_ A ) )
38 36 37 syl5ibr 
 |-  ( x e. RR -> ( A. y e. RR+ E. z e. RR+ ( z <_ y /\ ( ( x - z ) (,) ( x + z ) ) C_ A ) -> E. z e. RR+ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) z ) C_ A ) )
39 29 38 syl 
 |-  ( ( A C_ RR /\ x e. A ) -> ( A. y e. RR+ E. z e. RR+ ( z <_ y /\ ( ( x - z ) (,) ( x + z ) ) C_ A ) -> E. z e. RR+ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) z ) C_ A ) )
40 39 ralimdva 
 |-  ( A C_ RR -> ( A. x e. A A. y e. RR+ E. z e. RR+ ( z <_ y /\ ( ( x - z ) (,) ( x + z ) ) C_ A ) -> A. x e. A E. z e. RR+ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) z ) C_ A ) )
41 40 imdistani 
 |-  ( ( A C_ RR /\ A. x e. A A. y e. RR+ E. z e. RR+ ( z <_ y /\ ( ( x - z ) (,) ( x + z ) ) C_ A ) ) -> ( A C_ RR /\ A. x e. A E. z e. RR+ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) z ) C_ A ) )
42 4 elmopn2 
 |-  ( ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR ) -> ( A e. ( topGen ` ran (,) ) <-> ( A C_ RR /\ A. x e. A E. z e. RR+ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) z ) C_ A ) ) )
43 2 42 ax-mp 
 |-  ( A e. ( topGen ` ran (,) ) <-> ( A C_ RR /\ A. x e. A E. z e. RR+ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) z ) C_ A ) )
44 41 43 sylibr 
 |-  ( ( A C_ RR /\ A. x e. A A. y e. RR+ E. z e. RR+ ( z <_ y /\ ( ( x - z ) (,) ( x + z ) ) C_ A ) ) -> A e. ( topGen ` ran (,) ) )
45 28 44 impbii 
 |-  ( A e. ( topGen ` ran (,) ) <-> ( A C_ RR /\ A. x e. A A. y e. RR+ E. z e. RR+ ( z <_ y /\ ( ( x - z ) (,) ( x + z ) ) C_ A ) ) )