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		xmetunirn	$⊢ D \in ⋃ ran ∞Met \leftrightarrow D \in ∞Met (dom dom D)$
10	9	bilani	$⊢ (φ \land D \in ⋃ ran ∞Met) \to D \in ∞Met (dom dom D)$
11		eqid	$⊢ MetOpen (D) = MetOpen (D)$
12	11	mopnuni	$⊢ D \in ∞Met (dom dom D) \to dom dom D = ⋃ MetOpen (D)$
13	10 12	syl	$⊢ (φ \land D \in ⋃ ran ∞Met) \to dom dom D = ⋃ MetOpen (D)$
14	2	dmeqd	$⊢ φ \to dom D = dom ({dist (M) ↾}_{(X \times X)})$
15		dmres	$⊢ dom ({dist (M) ↾}_{(X \times X)}) = (X \times X) \cap dom dist (M)$
16	14 15	eqtrdi	$⊢ φ \to dom D = (X \times X) \cap dom dist (M)$
17		inss1	$⊢ (X \times X) \cap dom dist (M) \subseteq X \times X$
18	16 17	eqsstrdi	$⊢ φ \to dom D \subseteq X \times X$
19		dmss	$⊢ dom D \subseteq X \times X \to dom dom D \subseteq dom (X \times X)$
20	18 19	syl	$⊢ φ \to dom dom D \subseteq dom (X \times X)$
21		dmxpid	$⊢ dom (X \times X) = X$
22	20 21	sseqtrdi	$⊢ φ \to dom dom D \subseteq X$
23	22	adantr	$⊢ (φ \land D \in ⋃ ran ∞Met) \to dom dom D \subseteq X$
24	13 23	eqsstrrd	$⊢ (φ \land D \in ⋃ ran ∞Met) \to ⋃ MetOpen (D) \subseteq X$
25		sspwuni	$⊢ MetOpen (D) \subseteq 𝒫 X \leftrightarrow ⋃ MetOpen (D) \subseteq X$
26	24 25	sylibr	$⊢ (φ \land D \in ⋃ ran ∞Met) \to MetOpen (D) \subseteq 𝒫 X$
27	26	ex	$⊢ φ \to (D \in ⋃ ran ∞Met \to MetOpen (D) \subseteq 𝒫 X)$
28	8 27	syl5	$⊢ φ \to (D \in dom MetOpen \to MetOpen (D) \subseteq 𝒫 X)$
29		ndmfv	$⊢ \neg D \in dom MetOpen \to MetOpen (D) = \emptyset$
30		0ss	$⊢ \emptyset \subseteq 𝒫 X$
31	29 30	eqsstrdi	$⊢ \neg D \in dom MetOpen \to MetOpen (D) \subseteq 𝒫 X$
32	28 31	pm2.61d1	$⊢ φ \to MetOpen (D) \subseteq 𝒫 X$
33	1 2 3	setsmsbas	$⊢ φ \to X = {Base}_{K}$
34	33	pweqd	$⊢ φ \to 𝒫 X = 𝒫 {Base}_{K}$
35	32 5 34	3sstr3d	$⊢ φ \to TopSet (K) \subseteq 𝒫 {Base}_{K}$
36		eqid	$⊢ {Base}_{K} = {Base}_{K}$
37		eqid	$⊢ TopSet (K) = TopSet (K)$
38	36 37	topnid	$⊢ TopSet (K) \subseteq 𝒫 {Base}_{K} \to TopSet (K) = TopOpen (K)$
39	35 38	syl	$⊢ φ \to TopSet (K) = TopOpen (K)$
40	5 39	eqtrd	$⊢ φ \to MetOpen (D) = TopOpen (K)$

Metamath Proof Explorer

Theorem setsmstopn

Proof