Theorem setsmstopn

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

	Ref	Expression
Hypotheses	setsms.x	⊢ ( 𝜑 → 𝑋 = ( Base ‘ 𝑀 ) )
	setsms.d	⊢ ( 𝜑 → 𝐷 = ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) )
	setsms.k	⊢ ( 𝜑 → 𝐾 = ( 𝑀 sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ 𝐷 ) ⟩ ) )
	setsms.m	⊢ ( 𝜑 → 𝑀 ∈ 𝑉 )
Assertion	setsmstopn	⊢ ( 𝜑 → ( MetOpen ‘ 𝐷 ) = ( TopOpen ‘ 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		setsms.x	⊢ ( 𝜑 → 𝑋 = ( Base ‘ 𝑀 ) )
2		setsms.d	⊢ ( 𝜑 → 𝐷 = ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) )
3		setsms.k	⊢ ( 𝜑 → 𝐾 = ( 𝑀 sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ 𝐷 ) ⟩ ) )
4		setsms.m	⊢ ( 𝜑 → 𝑀 ∈ 𝑉 )
5	1 2 3 4	setsmstset	⊢ ( 𝜑 → ( MetOpen ‘ 𝐷 ) = ( TopSet ‘ 𝐾 ) )
6		df-mopn	⊢ MetOpen = ( 𝑥 ∈ ∪ ran ∞Met ↦ ( topGen ‘ ran ( ball ‘ 𝑥 ) ) )
7	6	dmmptss	⊢ dom MetOpen ⊆ ∪ ran ∞Met
8	7	sseli	⊢ ( 𝐷 ∈ dom MetOpen → 𝐷 ∈ ∪ ran ∞Met )
9		xmetunirn	⊢ ( 𝐷 ∈ ∪ ran ∞Met ↔ 𝐷 ∈ ( ∞Met ‘ dom dom 𝐷 ) )
10	9	bilani	⊢ ( ( 𝜑 ∧ 𝐷 ∈ ∪ ran ∞Met ) → 𝐷 ∈ ( ∞Met ‘ dom dom 𝐷 ) )
11		eqid	⊢ ( MetOpen ‘ 𝐷 ) = ( MetOpen ‘ 𝐷 )
12	11	mopnuni	⊢ ( 𝐷 ∈ ( ∞Met ‘ dom dom 𝐷 ) → dom dom 𝐷 = ∪ ( MetOpen ‘ 𝐷 ) )
13	10 12	syl	⊢ ( ( 𝜑 ∧ 𝐷 ∈ ∪ ran ∞Met ) → dom dom 𝐷 = ∪ ( MetOpen ‘ 𝐷 ) )
14	2	dmeqd	⊢ ( 𝜑 → dom 𝐷 = dom ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) )
15		dmres	⊢ dom ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) = ( ( 𝑋 × 𝑋 ) ∩ dom ( dist ‘ 𝑀 ) )
16	14 15	eqtrdi	⊢ ( 𝜑 → dom 𝐷 = ( ( 𝑋 × 𝑋 ) ∩ dom ( dist ‘ 𝑀 ) ) )
17		inss1	⊢ ( ( 𝑋 × 𝑋 ) ∩ dom ( dist ‘ 𝑀 ) ) ⊆ ( 𝑋 × 𝑋 )
18	16 17	eqsstrdi	⊢ ( 𝜑 → dom 𝐷 ⊆ ( 𝑋 × 𝑋 ) )
19		dmss	⊢ ( dom 𝐷 ⊆ ( 𝑋 × 𝑋 ) → dom dom 𝐷 ⊆ dom ( 𝑋 × 𝑋 ) )
20	18 19	syl	⊢ ( 𝜑 → dom dom 𝐷 ⊆ dom ( 𝑋 × 𝑋 ) )
21		dmxpid	⊢ dom ( 𝑋 × 𝑋 ) = 𝑋
22	20 21	sseqtrdi	⊢ ( 𝜑 → dom dom 𝐷 ⊆ 𝑋 )
23	22	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ∈ ∪ ran ∞Met ) → dom dom 𝐷 ⊆ 𝑋 )
24	13 23	eqsstrrd	⊢ ( ( 𝜑 ∧ 𝐷 ∈ ∪ ran ∞Met ) → ∪ ( MetOpen ‘ 𝐷 ) ⊆ 𝑋 )
25		sspwuni	⊢ ( ( MetOpen ‘ 𝐷 ) ⊆ 𝒫 𝑋 ↔ ∪ ( MetOpen ‘ 𝐷 ) ⊆ 𝑋 )
26	24 25	sylibr	⊢ ( ( 𝜑 ∧ 𝐷 ∈ ∪ ran ∞Met ) → ( MetOpen ‘ 𝐷 ) ⊆ 𝒫 𝑋 )
27	26	ex	⊢ ( 𝜑 → ( 𝐷 ∈ ∪ ran ∞Met → ( MetOpen ‘ 𝐷 ) ⊆ 𝒫 𝑋 ) )
28	8 27	syl5	⊢ ( 𝜑 → ( 𝐷 ∈ dom MetOpen → ( MetOpen ‘ 𝐷 ) ⊆ 𝒫 𝑋 ) )
29		ndmfv	⊢ ( ¬ 𝐷 ∈ dom MetOpen → ( MetOpen ‘ 𝐷 ) = ∅ )
30		0ss	⊢ ∅ ⊆ 𝒫 𝑋
31	29 30	eqsstrdi	⊢ ( ¬ 𝐷 ∈ dom MetOpen → ( MetOpen ‘ 𝐷 ) ⊆ 𝒫 𝑋 )
32	28 31	pm2.61d1	⊢ ( 𝜑 → ( MetOpen ‘ 𝐷 ) ⊆ 𝒫 𝑋 )
33	1 2 3	setsmsbas	⊢ ( 𝜑 → 𝑋 = ( Base ‘ 𝐾 ) )
34	33	pweqd	⊢ ( 𝜑 → 𝒫 𝑋 = 𝒫 ( Base ‘ 𝐾 ) )
35	32 5 34	3sstr3d	⊢ ( 𝜑 → ( TopSet ‘ 𝐾 ) ⊆ 𝒫 ( Base ‘ 𝐾 ) )
36		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
37		eqid	⊢ ( TopSet ‘ 𝐾 ) = ( TopSet ‘ 𝐾 )
38	36 37	topnid	⊢ ( ( TopSet ‘ 𝐾 ) ⊆ 𝒫 ( Base ‘ 𝐾 ) → ( TopSet ‘ 𝐾 ) = ( TopOpen ‘ 𝐾 ) )
39	35 38	syl	⊢ ( 𝜑 → ( TopSet ‘ 𝐾 ) = ( TopOpen ‘ 𝐾 ) )
40	5 39	eqtrd	⊢ ( 𝜑 → ( MetOpen ‘ 𝐷 ) = ( TopOpen ‘ 𝐾 ) )