Metamath Proof Explorer

Theorem setsmsbas

Description: The base set 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 setsmsbas 
|- ( ph -> X = ( Base ` 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 baseid 
 |-  Base = Slot ( Base ` ndx )
5 1re 
 |-  1 e. RR
6 1lt9 
 |-  1 < 9
7 5 6 ltneii 
 |-  1 =/= 9
8 basendx 
 |-  ( Base ` ndx ) = 1
9 tsetndx 
 |-  ( TopSet ` ndx ) = 9
10 8 9 neeq12i 
 |-  ( ( Base ` ndx ) =/= ( TopSet ` ndx ) <-> 1 =/= 9 )
11 7 10 mpbir 
 |-  ( Base ` ndx ) =/= ( TopSet ` ndx )
12 4 11 setsnid 
 |-  ( Base ` M ) = ( Base ` ( M sSet <. ( TopSet ` ndx ) , ( MetOpen ` D ) >. ) )
13 3 fveq2d 
 |-  ( ph -> ( Base ` K ) = ( Base ` ( M sSet <. ( TopSet ` ndx ) , ( MetOpen ` D ) >. ) ) )
14 12 1 13 3eqtr4a 
 |-  ( ph -> X = ( Base ` K ) )