Metamath Proof Explorer

Theorem setsmstset

Description: The topology 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 ) >. ) )
setsms.m 
|- ( ph -> M e. V )
Assertion setsmstset 
|- ( ph -> ( MetOpen ` D ) = ( TopSet ` 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 setsms.m 
 |-  ( ph -> M e. V )
5 fvex 
 |-  ( MetOpen ` D ) e. _V
6 tsetid 
 |-  TopSet = Slot ( TopSet ` ndx )
7 6 setsid 
 |-  ( ( M e. V /\ ( MetOpen ` D ) e. _V ) -> ( MetOpen ` D ) = ( TopSet ` ( M sSet <. ( TopSet ` ndx ) , ( MetOpen ` D ) >. ) ) )
8 4 5 7 sylancl 
 |-  ( ph -> ( MetOpen ` D ) = ( TopSet ` ( M sSet <. ( TopSet ` ndx ) , ( MetOpen ` D ) >. ) ) )
9 3 fveq2d 
 |-  ( ph -> ( TopSet ` K ) = ( TopSet ` ( M sSet <. ( TopSet ` ndx ) , ( MetOpen ` D ) >. ) ) )
10 8 9 eqtr4d 
 |-  ( ph -> ( MetOpen ` D ) = ( TopSet ` K ) )