setsmstopn

Description: The topology of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015)

	Ref	Expression
Hypotheses	setsms.x	$⊢ φ \to X = {Base}_{M}$
	setsms.d	$⊢ φ \to D = {dist (M) ↾}_{(X \times X)}$
	setsms.k	$⊢ φ \to K = M sSet ⟨TopSet (ndx), MetOpen (D)⟩$
	setsms.m	$⊢ φ \to M \in V$
Assertion	setsmstopn	$⊢ φ \to MetOpen (D) = TopOpen (K)$

Proof

Step	Hyp	Ref	Expression
1		setsms.x	$⊢ φ \to X = {Base}_{M}$
2		setsms.d	$⊢ φ \to D = {dist (M) ↾}_{(X \times X)}$
3		setsms.k	$⊢ φ \to K = M sSet ⟨TopSet (ndx), MetOpen (D)⟩$
4		setsms.m	$⊢ φ \to M \in V$
5	1 2 3 4	setsmstset	$⊢ φ \to MetOpen (D) = TopSet (K)$
6		df-mopn	$⊢ MetOpen = (x \in ⋃ ran ∞Met ⟼ topGen (ran ball (x)))$
7	6	dmmptss	$⊢ dom MetOpen \subseteq ⋃ ran ∞Met$
8	7	sseli	$⊢ D \in dom MetOpen \to D \in ⋃ ran ∞Met$
9		simpr	$⊢ (φ \land D \in ⋃ ran ∞Met) \to D \in ⋃ ran ∞Met$
10		xmetunirn	$⊢ D \in ⋃ ran ∞Met \leftrightarrow D \in ∞Met (dom dom D)$
11	9 10	sylib	$⊢ (φ \land D \in ⋃ ran ∞Met) \to D \in ∞Met (dom dom D)$
12		eqid	$⊢ MetOpen (D) = MetOpen (D)$
13	12	mopnuni	$⊢ D \in ∞Met (dom dom D) \to dom dom D = ⋃ MetOpen (D)$
14	11 13	syl	$⊢ (φ \land D \in ⋃ ran ∞Met) \to dom dom D = ⋃ MetOpen (D)$
15	2	dmeqd	$⊢ φ \to dom D = dom ({dist (M) ↾}_{(X \times X)})$
16		dmres	$⊢ dom ({dist (M) ↾}_{(X \times X)}) = (X \times X) \cap dom dist (M)$
17	15 16	eqtrdi	$⊢ φ \to dom D = (X \times X) \cap dom dist (M)$
18		inss1	$⊢ (X \times X) \cap dom dist (M) \subseteq X \times X$
19	17 18	eqsstrdi	$⊢ φ \to dom D \subseteq X \times X$
20		dmss	$⊢ dom D \subseteq X \times X \to dom dom D \subseteq dom (X \times X)$
21	19 20	syl	$⊢ φ \to dom dom D \subseteq dom (X \times X)$
22		dmxpid	$⊢ dom (X \times X) = X$
23	21 22	sseqtrdi	$⊢ φ \to dom dom D \subseteq X$
24	23	adantr	$⊢ (φ \land D \in ⋃ ran ∞Met) \to dom dom D \subseteq X$
25	14 24	eqsstrrd	$⊢ (φ \land D \in ⋃ ran ∞Met) \to ⋃ MetOpen (D) \subseteq X$
26		sspwuni	$⊢ MetOpen (D) \subseteq 𝒫 X \leftrightarrow ⋃ MetOpen (D) \subseteq X$
27	25 26	sylibr	$⊢ (φ \land D \in ⋃ ran ∞Met) \to MetOpen (D) \subseteq 𝒫 X$
28	27	ex	$⊢ φ \to (D \in ⋃ ran ∞Met \to MetOpen (D) \subseteq 𝒫 X)$
29	8 28	syl5	$⊢ φ \to (D \in dom MetOpen \to MetOpen (D) \subseteq 𝒫 X)$
30		ndmfv	$⊢ \neg D \in dom MetOpen \to MetOpen (D) = \emptyset$
31		0ss	$⊢ \emptyset \subseteq 𝒫 X$
32	30 31	eqsstrdi	$⊢ \neg D \in dom MetOpen \to MetOpen (D) \subseteq 𝒫 X$
33	29 32	pm2.61d1	$⊢ φ \to MetOpen (D) \subseteq 𝒫 X$
34	1 2 3	setsmsbas	$⊢ φ \to X = {Base}_{K}$
35	34	pweqd	$⊢ φ \to 𝒫 X = 𝒫 {Base}_{K}$
36	33 5 35	3sstr3d	$⊢ φ \to TopSet (K) \subseteq 𝒫 {Base}_{K}$
37		eqid	$⊢ {Base}_{K} = {Base}_{K}$
38		eqid	$⊢ TopSet (K) = TopSet (K)$
39	37 38	topnid	$⊢ TopSet (K) \subseteq 𝒫 {Base}_{K} \to TopSet (K) = TopOpen (K)$
40	36 39	syl	$⊢ φ \to TopSet (K) = TopOpen (K)$
41	5 40	eqtrd	$⊢ φ \to MetOpen (D) = TopOpen (K)$

Metamath Proof Explorer

Theorem setsmstopn

Proof