Theorem tmsbas

Description: The base set of a constructed metric space. (Contributed by Mario Carneiro, 2-Sep-2015)

	Ref	Expression
Hypothesis	tmsbas.k	|- K = ( toMetSp ` D )
Assertion	tmsbas	|- ( D e. ( *Met ` X ) -> X = ( Base ` K ) )

Proof

Step	Hyp	Ref	Expression
1		tmsbas.k	|- K = ( toMetSp ` D )
2		eqid	|- { <. ( Base ` ndx ) , X >. , <. ( dist ` ndx ) , D >. } = { <. ( Base ` ndx ) , X >. , <. ( dist ` ndx ) , D >. }
3	2 1	tmslem	|- ( D e. ( *Met ` X ) -> ( X = ( Base ` K ) /\ D = ( dist ` K ) /\ ( MetOpen ` D ) = ( TopOpen ` K ) ) )
4	3	simp1d	|- ( D e. ( *Met ` X ) -> X = ( Base ` K ) )