mopntopon

Description: The set of open sets of a metric space X is a topology on X . Remark in Kreyszig p. 19. This theorem connects the two concepts and makes available the theorems for topologies for use with metric spaces. (Contributed by Mario Carneiro, 24-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		mopnval.1	$⊢ J = MetOpen (D)$
2	1	mopnval	$⊢ D \in ∞Met (X) \to J = topGen (ran ball (D))$
3		blbas	$⊢ D \in ∞Met (X) \to ran ball (D) \in TopBases$
4		tgtopon	$⊢ ran ball (D) \in TopBases \to topGen (ran ball (D)) \in TopOn (⋃ ran ball (D))$
5	3 4	syl	$⊢ D \in ∞Met (X) \to topGen (ran ball (D)) \in TopOn (⋃ ran ball (D))$
6		unirnbl	$⊢ D \in ∞Met (X) \to ⋃ ran ball (D) = X$
7	6	fveq2d	$⊢ D \in ∞Met (X) \to TopOn (⋃ ran ball (D)) = TopOn (X)$
8	5 7	eleqtrd	$⊢ D \in ∞Met (X) \to topGen (ran ball (D)) \in TopOn (X)$
9	2 8	eqeltrd	$⊢ D \in ∞Met (X) \to J \in TopOn (X)$

Metamath Proof Explorer

Theorem mopntopon

Proof