Theorem mopni

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

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

Proof

Step	Hyp	Ref	Expression
1		mopni.1	|- J = ( MetOpen ` D )
2	1	elmopn	|- ( D e. ( *Met ` X ) -> ( A e. J <-> ( A C_ X /\ A. y e. A E. x e. ran ( ball ` D ) ( y e. x /\ x C_ A ) ) ) )
3	2	simplbda	|- ( ( D e. ( *Met ` X ) /\ A e. J ) -> A. y e. A E. x e. ran ( ball ` D ) ( y e. x /\ x C_ A ) )
4		eleq1	|- ( y = P -> ( y e. x <-> P e. x ) )
5	4	anbi1d	|- ( y = P -> ( ( y e. x /\ x C_ A ) <-> ( P e. x /\ x C_ A ) ) )
6	5	rexbidv	|- ( y = P -> ( E. x e. ran ( ball ` D ) ( y e. x /\ x C_ A ) <-> E. x e. ran ( ball ` D ) ( P e. x /\ x C_ A ) ) )
7	6	rspccv	|- ( A. y e. A E. x e. ran ( ball ` D ) ( y e. x /\ x C_ A ) -> ( P e. A -> E. x e. ran ( ball ` D ) ( P e. x /\ x C_ A ) ) )
8	3 7	syl	|- ( ( D e. ( *Met ` X ) /\ A e. J ) -> ( P e. A -> E. x e. ran ( ball ` D ) ( P e. x /\ x C_ A ) ) )
9	8	3impia	|- ( ( D e. ( *Met ` X ) /\ A e. J /\ P e. A ) -> E. x e. ran ( ball ` D ) ( P e. x /\ x C_ A ) )