Theorem setsmsbasOLD

Description: Obsolete version of setsmsbas as of 12-Nov-2024. The base set of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	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	setsmsbasOLD	|- ( 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 ) )