Theorem setsmsdsOLD

Description: Obsolete proof of setsmsds as of 11-Nov-2024. The distance function 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	setsmsdsOLD	|- ( 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 ) )