mopnval

Description: An open set is a subset of a metric space which includes a ball around each of its points. Definition 1.3-2 of Kreyszig p. 18. The object ( MetOpenD ) is the family of all open sets in the metric space determined by the metric D . By mopntop , the open sets of a metric space form a topology J , whose base set is U. J by mopnuni . (Contributed by NM, 1-Sep-2006) (Revised by Mario Carneiro, 12-Nov-2013)

		Ref	Expression
	Hypothesis	mopnval.1	$⊢ J = MetOpen (D)$
	Assertion	mopnval	$⊢ D \in ∞Met (X) \to J = topGen (ran ball (D))$

Proof

Step	Hyp	Ref	Expression
1		mopnval.1	$⊢ J = MetOpen (D)$
2		fvssunirn	$⊢ ∞Met (X) \subseteq ⋃ ran ∞Met$
3	2	sseli	$⊢ D \in ∞Met (X) \to D \in ⋃ ran ∞Met$
4		fveq2	$⊢ d = D \to ball (d) = ball (D)$
5	4	rneqd	$⊢ d = D \to ran ball (d) = ran ball (D)$
6	5	fveq2d	$⊢ d = D \to topGen (ran ball (d)) = topGen (ran ball (D))$
7		df-mopn	$⊢ MetOpen = (d \in ⋃ ran ∞Met ⟼ topGen (ran ball (d)))$
8		fvex	$⊢ topGen (ran ball (D)) \in V$
9	6 7 8	fvmpt	$⊢ D \in ⋃ ran ∞Met \to MetOpen (D) = topGen (ran ball (D))$
10	1 9	eqtrid	$⊢ D \in ⋃ ran ∞Met \to J = topGen (ran ball (D))$
11	3 10	syl	$⊢ D \in ∞Met (X) \to J = topGen (ran ball (D))$

Metamath Proof Explorer

Theorem mopnval

Proof