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