elmopn2

Description: A defining property of an open set of a metric space. (Contributed by NM, 5-May-2007) (Revised by Mario Carneiro, 12-Nov-2013)

		Ref	Expression
	Hypothesis	mopnval.1	$⊢ J = MetOpen (D)$
	Assertion	elmopn2	$⊢ D \in ∞Met (X) \to (A \in J \leftrightarrow (A \subseteq X \land \forall x \in A \exists y \in ℝ^{+} x ball (D) y \subseteq A))$

Step	Hyp	Ref	Expression
1		mopnval.1	$⊢ J = MetOpen (D)$
2	1	elmopn	$⊢ D \in ∞Met (X) \to (A \in J \leftrightarrow (A \subseteq X \land \forall x \in A \exists z \in ran ball (D) (x \in z \land z \subseteq A)))$
3		ssel2	$⊢ (A \subseteq X \land x \in A) \to x \in X$
4		blssex	$⊢ (D \in ∞Met (X) \land x \in X) \to (\exists z \in ran ball (D) (x \in z \land z \subseteq A) \leftrightarrow \exists y \in ℝ^{+} x ball (D) y \subseteq A)$
5	3 4	sylan2	$⊢ (D \in ∞Met (X) \land (A \subseteq X \land x \in A)) \to (\exists z \in ran ball (D) (x \in z \land z \subseteq A) \leftrightarrow \exists y \in ℝ^{+} x ball (D) y \subseteq A)$
6	5	anassrs	$⊢ ((D \in ∞Met (X) \land A \subseteq X) \land x \in A) \to (\exists z \in ran ball (D) (x \in z \land z \subseteq A) \leftrightarrow \exists y \in ℝ^{+} x ball (D) y \subseteq A)$
7	6	ralbidva	$⊢ (D \in ∞Met (X) \land A \subseteq X) \to (\forall x \in A \exists z \in ran ball (D) (x \in z \land z \subseteq A) \leftrightarrow \forall x \in A \exists y \in ℝ^{+} x ball (D) y \subseteq A)$
8	7	pm5.32da	$⊢ D \in ∞Met (X) \to ((A \subseteq X \land \forall x \in A \exists z \in ran ball (D) (x \in z \land z \subseteq A)) \leftrightarrow (A \subseteq X \land \forall x \in A \exists y \in ℝ^{+} x ball (D) y \subseteq A))$
9	2 8	bitrd	$⊢ D \in ∞Met (X) \to (A \in J \leftrightarrow (A \subseteq X \land \forall x \in A \exists y \in ℝ^{+} x ball (D) y \subseteq A))$

Metamath Proof Explorer