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 df-ds dist = Slot 12
5 1nn 1
6 2nn0 2 0
7 1nn0 1 0
8 1lt10 1 < 10
9 5 6 7 8 declti 1 < 12
10 2nn 2
11 7 10 decnncl 12
12 1 4 9 11 2strbas X dom ∞Met X = Base M
13 3 12 syl D ∞Met X X = Base M
14 xmetf D ∞Met X D : X × X *
15 ffn D : X × X * D Fn X × X
16 fnresdm D Fn X × X D X × X = D
17 14 15 16 3syl D ∞Met X D X × X = D
18 1 4 9 11 2strop D ∞Met X D = dist M
19 18 reseq1d D ∞Met X D X × X = dist M X × X
20 17 19 eqtr3d D ∞Met X D = dist M X × X
21 1 2 tmsval D ∞Met X K = M sSet TopSet ndx MetOpen D
22 13 20 21 setsmsbas D ∞Met X X = Base K
23 13 20 21 setsmsds D ∞Met X dist M = dist K
24 18 23 eqtrd D ∞Met X D = dist K
25 prex Base ndx X dist ndx D V
26 1 25 eqeltri M V
27 26 a1i D ∞Met X M V
28 13 20 21 27 setsmstopn D ∞Met X MetOpen D = TopOpen K
29 22 24 28 3jca D ∞Met X X = Base K D = dist K MetOpen D = TopOpen K