This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem setsmstset

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

Ref Expression
Hypotheses setsms.x ⊢ φ → X = Base M
setsms.d ⊢ φ → D = dist ⁡ M ↾ X × X
setsms.k ⊢ φ → K = M sSet TopSet ⁡ ndx MetOpen ⁡ D
setsms.m ⊢ φ → M ∈ V
Assertion setsmstset ⊢ φ → MetOpen ⁡ D = TopSet ⁡ K

Proof

Step Hyp Ref Expression
1 setsms.x ⊢ φ → X = Base M
2 setsms.d ⊢ φ → D = dist ⁡ M ↾ X × X
3 setsms.k ⊢ φ → K = M sSet TopSet ⁡ ndx MetOpen ⁡ D
4 setsms.m ⊢ φ → M ∈ V
5 fvex ⊢ MetOpen ⁡ D ∈ V
6 tsetid ⊢ TopSet = Slot TopSet ⁡ ndx
7 6 setsid ⊢ M ∈ V ∧ MetOpen ⁡ D ∈ V → MetOpen ⁡ D = TopSet ⁡ M sSet TopSet ⁡ ndx MetOpen ⁡ D
8 4 5 7 sylancl ⊢ φ → MetOpen ⁡ D = TopSet ⁡ M sSet TopSet ⁡ ndx MetOpen ⁡ D
9 3 fveq2d ⊢ φ → TopSet ⁡ K = TopSet ⁡ M sSet TopSet ⁡ ndx MetOpen ⁡ D
10 8 9 eqtr4d ⊢ φ → MetOpen ⁡ D = TopSet ⁡ K