Metamath Proof Explorer


Theorem tmslem

Description: Lemma for tmsbas , tmsds , and tmstopn . (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses tmsval.m M = Base ndx X dist ndx D
tmsval.k K = toMetSp D
Assertion tmslem D ∞Met X X = Base K D = dist K MetOpen D = TopOpen K

Proof

Step Hyp Ref Expression
1 tmsval.m M = Base ndx X dist ndx D
2 tmsval.k K = toMetSp D
3 elfvdm D ∞Met X X dom ∞Met
4 basendxltdsndx Base ndx < dist ndx
5 dsndxnn dist ndx
6 1 4 5 2strbas1 X dom ∞Met X = Base M
7 3 6 syl D ∞Met X X = Base M
8 xmetf D ∞Met X D : X × X *
9 ffn D : X × X * D Fn X × X
10 fnresdm D Fn X × X D X × X = D
11 8 9 10 3syl D ∞Met X D X × X = D
12 dsid dist = Slot dist ndx
13 1 4 5 12 2strop1 D ∞Met X D = dist M
14 13 reseq1d D ∞Met X D X × X = dist M X × X
15 11 14 eqtr3d D ∞Met X D = dist M X × X
16 1 2 tmsval D ∞Met X K = M sSet TopSet ndx MetOpen D
17 7 15 16 setsmsbas D ∞Met X X = Base K
18 7 15 16 setsmsds D ∞Met X dist M = dist K
19 13 18 eqtrd D ∞Met X D = dist K
20 prex Base ndx X dist ndx D V
21 1 20 eqeltri M V
22 21 a1i D ∞Met X M V
23 7 15 16 22 setsmstopn D ∞Met X MetOpen D = TopOpen K
24 17 19 23 3jca D ∞Met X X = Base K D = dist K MetOpen D = TopOpen K