Metamath Proof Explorer

Theorem mopni3

Description: An open set of a metric space includes an arbitrarily small ball around each of its points. (Contributed by NM, 20-Sep-2007) (Revised by Mario Carneiro, 12-Nov-2013)

Ref Expression
Hypothesis mopni.1 
|- J = ( MetOpen ` D )
Assertion mopni3 
|- ( ( ( D e. ( *Met ` X ) /\ A e. J /\ P e. A ) /\ R e. RR+ ) -> E. x e. RR+ ( x < R /\ ( P ( ball ` D ) x ) C_ A ) )

Proof

Step Hyp Ref Expression
1 mopni.1 
 |-  J = ( MetOpen ` D )
2 1 mopni2 
 |-  ( ( D e. ( *Met ` X ) /\ A e. J /\ P e. A ) -> E. y e. RR+ ( P ( ball ` D ) y ) C_ A )
3 2 adantr 
 |-  ( ( ( D e. ( *Met ` X ) /\ A e. J /\ P e. A ) /\ R e. RR+ ) -> E. y e. RR+ ( P ( ball ` D ) y ) C_ A )
4 simp1 
 |-  ( ( D e. ( *Met ` X ) /\ A e. J /\ P e. A ) -> D e. ( *Met ` X ) )
5 1 mopnss 
 |-  ( ( D e. ( *Met ` X ) /\ A e. J ) -> A C_ X )
6 5 sselda 
 |-  ( ( ( D e. ( *Met ` X ) /\ A e. J ) /\ P e. A ) -> P e. X )
7 6 3impa 
 |-  ( ( D e. ( *Met ` X ) /\ A e. J /\ P e. A ) -> P e. X )
8 4 7 jca 
 |-  ( ( D e. ( *Met ` X ) /\ A e. J /\ P e. A ) -> ( D e. ( *Met ` X ) /\ P e. X ) )
9 ssblex 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR+ /\ y e. RR+ ) ) -> E. x e. RR+ ( x < R /\ ( P ( ball ` D ) x ) C_ ( P ( ball ` D ) y ) ) )
10 8 9 sylan 
 |-  ( ( ( D e. ( *Met ` X ) /\ A e. J /\ P e. A ) /\ ( R e. RR+ /\ y e. RR+ ) ) -> E. x e. RR+ ( x < R /\ ( P ( ball ` D ) x ) C_ ( P ( ball ` D ) y ) ) )
11 10 anassrs 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ A e. J /\ P e. A ) /\ R e. RR+ ) /\ y e. RR+ ) -> E. x e. RR+ ( x < R /\ ( P ( ball ` D ) x ) C_ ( P ( ball ` D ) y ) ) )
12 sstr 
 |-  ( ( ( P ( ball ` D ) x ) C_ ( P ( ball ` D ) y ) /\ ( P ( ball ` D ) y ) C_ A ) -> ( P ( ball ` D ) x ) C_ A )
13 12 expcom 
 |-  ( ( P ( ball ` D ) y ) C_ A -> ( ( P ( ball ` D ) x ) C_ ( P ( ball ` D ) y ) -> ( P ( ball ` D ) x ) C_ A ) )
14 13 anim2d 
 |-  ( ( P ( ball ` D ) y ) C_ A -> ( ( x < R /\ ( P ( ball ` D ) x ) C_ ( P ( ball ` D ) y ) ) -> ( x < R /\ ( P ( ball ` D ) x ) C_ A ) ) )
15 14 reximdv 
 |-  ( ( P ( ball ` D ) y ) C_ A -> ( E. x e. RR+ ( x < R /\ ( P ( ball ` D ) x ) C_ ( P ( ball ` D ) y ) ) -> E. x e. RR+ ( x < R /\ ( P ( ball ` D ) x ) C_ A ) ) )
16 11 15 syl5com 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ A e. J /\ P e. A ) /\ R e. RR+ ) /\ y e. RR+ ) -> ( ( P ( ball ` D ) y ) C_ A -> E. x e. RR+ ( x < R /\ ( P ( ball ` D ) x ) C_ A ) ) )
17 16 rexlimdva 
 |-  ( ( ( D e. ( *Met ` X ) /\ A e. J /\ P e. A ) /\ R e. RR+ ) -> ( E. y e. RR+ ( P ( ball ` D ) y ) C_ A -> E. x e. RR+ ( x < R /\ ( P ( ball ` D ) x ) C_ A ) ) )
18 3 17 mpd 
 |-  ( ( ( D e. ( *Met ` X ) /\ A e. J /\ P e. A ) /\ R e. RR+ ) -> E. x e. RR+ ( x < R /\ ( P ( ball ` D ) x ) C_ A ) )