Metamath Proof Explorer

Theorem opnrebl

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

Ref Expression
Assertion opnrebl 
|- ( A e. ( topGen ` ran (,) ) <-> ( A C_ RR /\ A. x e. A E. y e. RR+ ( ( x - y ) (,) ( x + y ) ) 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 elmopn2 
 |-  ( ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR ) -> ( A e. ( topGen ` ran (,) ) <-> ( A C_ RR /\ A. x e. A E. y e. RR+ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) y ) C_ A ) ) )
6 2 5 ax-mp 
 |-  ( A e. ( topGen ` ran (,) ) <-> ( A C_ RR /\ A. x e. A E. y e. RR+ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) y ) C_ A ) )
7 ssel2 
 |-  ( ( A C_ RR /\ x e. A ) -> x e. RR )
8 rpre 
 |-  ( y e. RR+ -> y e. RR )
9 1 bl2ioo 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) y ) = ( ( x - y ) (,) ( x + y ) ) )
10 8 9 sylan2 
 |-  ( ( x e. RR /\ y e. RR+ ) -> ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) y ) = ( ( x - y ) (,) ( x + y ) ) )
11 10 sseq1d 
 |-  ( ( x e. RR /\ y e. RR+ ) -> ( ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) y ) C_ A <-> ( ( x - y ) (,) ( x + y ) ) C_ A ) )
12 11 rexbidva 
 |-  ( x e. RR -> ( E. y e. RR+ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) y ) C_ A <-> E. y e. RR+ ( ( x - y ) (,) ( x + y ) ) C_ A ) )
13 7 12 syl 
 |-  ( ( A C_ RR /\ x e. A ) -> ( E. y e. RR+ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) y ) C_ A <-> E. y e. RR+ ( ( x - y ) (,) ( x + y ) ) C_ A ) )
14 13 ralbidva 
 |-  ( A C_ RR -> ( A. x e. A E. y e. RR+ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) y ) C_ A <-> A. x e. A E. y e. RR+ ( ( x - y ) (,) ( x + y ) ) C_ A ) )
15 14 pm5.32i 
 |-  ( ( A C_ RR /\ A. x e. A E. y e. RR+ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) y ) C_ A ) <-> ( A C_ RR /\ A. x e. A E. y e. RR+ ( ( x - y ) (,) ( x + y ) ) C_ A ) )
16 6 15 bitri 
 |-  ( A e. ( topGen ` ran (,) ) <-> ( A C_ RR /\ A. x e. A E. y e. RR+ ( ( x - y ) (,) ( x + y ) ) C_ A ) )