Metamath Proof Explorer

Theorem setsmsds

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

Ref Expression
Hypotheses setsms.x 
|- ( ph -> X = ( Base ` M ) )
setsms.d 
|- ( ph -> D = ( ( dist ` M ) |` ( X X. X ) ) )
setsms.k 
|- ( ph -> K = ( M sSet <. ( TopSet ` ndx ) , ( MetOpen ` D ) >. ) )
Assertion setsmsds 
|- ( ph -> ( dist ` M ) = ( dist ` K ) )

Proof

Step Hyp Ref Expression
1 setsms.x 
 |-  ( ph -> X = ( Base ` M ) )
2 setsms.d 
 |-  ( ph -> D = ( ( dist ` M ) |` ( X X. X ) ) )
3 setsms.k 
 |-  ( ph -> K = ( M sSet <. ( TopSet ` ndx ) , ( MetOpen ` D ) >. ) )
4 dsid 
 |-  dist = Slot ( dist ` ndx )
5 9re 
 |-  9 e. RR
6 1nn 
 |-  1 e. NN
7 2nn0 
 |-  2 e. NN0
8 9nn0 
 |-  9 e. NN0
9 9lt10 
 |-  9 < ; 1 0
10 6 7 8 9 declti 
 |-  9 < ; 1 2
11 5 10 gtneii 
 |-  ; 1 2 =/= 9
12 dsndx 
 |-  ( dist ` ndx ) = ; 1 2
13 tsetndx 
 |-  ( TopSet ` ndx ) = 9
14 12 13 neeq12i 
 |-  ( ( dist ` ndx ) =/= ( TopSet ` ndx ) <-> ; 1 2 =/= 9 )
15 11 14 mpbir 
 |-  ( dist ` ndx ) =/= ( TopSet ` ndx )
16 4 15 setsnid 
 |-  ( dist ` M ) = ( dist ` ( M sSet <. ( TopSet ` ndx ) , ( MetOpen ` D ) >. ) )
17 3 fveq2d 
 |-  ( ph -> ( dist ` K ) = ( dist ` ( M sSet <. ( TopSet ` ndx ) , ( MetOpen ` D ) >. ) ) )
18 16 17 eqtr4id 
 |-  ( ph -> ( dist ` M ) = ( dist ` K ) )