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 e. ( *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 e. ( *Met ` X ) -> X e. dom *Met )
4 basendxltdsndx 
 |-  ( Base ` ndx ) < ( dist ` ndx )
5 dsndxnn 
 |-  ( dist ` ndx ) e. NN
6 1 4 5 2strbas1 
 |-  ( X e. dom *Met -> X = ( Base ` M ) )
7 3 6 syl 
 |-  ( D e. ( *Met ` X ) -> X = ( Base ` M ) )
8 xmetf 
 |-  ( D e. ( *Met ` X ) -> D : ( X X. X ) --> RR* )
9 ffn 
 |-  ( D : ( X X. X ) --> RR* -> D Fn ( X X. X ) )
10 fnresdm 
 |-  ( D Fn ( X X. X ) -> ( D |` ( X X. X ) ) = D )
11 8 9 10 3syl 
 |-  ( D e. ( *Met ` X ) -> ( D |` ( X X. X ) ) = D )
12 dsid 
 |-  dist = Slot ( dist ` ndx )
13 1 4 5 12 2strop1 
 |-  ( D e. ( *Met ` X ) -> D = ( dist ` M ) )
14 13 reseq1d 
 |-  ( D e. ( *Met ` X ) -> ( D |` ( X X. X ) ) = ( ( dist ` M ) |` ( X X. X ) ) )
15 11 14 eqtr3d 
 |-  ( D e. ( *Met ` X ) -> D = ( ( dist ` M ) |` ( X X. X ) ) )
16 1 2 tmsval 
 |-  ( D e. ( *Met ` X ) -> K = ( M sSet <. ( TopSet ` ndx ) , ( MetOpen ` D ) >. ) )
17 7 15 16 setsmsbas 
 |-  ( D e. ( *Met ` X ) -> X = ( Base ` K ) )
18 7 15 16 setsmsds 
 |-  ( D e. ( *Met ` X ) -> ( dist ` M ) = ( dist ` K ) )
19 13 18 eqtrd 
 |-  ( D e. ( *Met ` X ) -> D = ( dist ` K ) )
20 prex 
 |-  { <. ( Base ` ndx ) , X >. , <. ( dist ` ndx ) , D >. } e. _V
21 1 20 eqeltri 
 |-  M e. _V
22 21 a1i 
 |-  ( D e. ( *Met ` X ) -> M e. _V )
23 7 15 16 22 setsmstopn 
 |-  ( D e. ( *Met ` X ) -> ( MetOpen ` D ) = ( TopOpen ` K ) )
24 17 19 23 3jca 
 |-  ( D e. ( *Met ` X ) -> ( X = ( Base ` K ) /\ D = ( dist ` K ) /\ ( MetOpen ` D ) = ( TopOpen ` K ) ) )