Theorem tmstopn

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

	Ref	Expression
Hypotheses	tmsbas.k	|- K = ( toMetSp ` D )
	tmstopn.j	|- J = ( MetOpen ` D )
Assertion	tmstopn	|- ( D e. ( *Met ` X ) -> J = ( TopOpen ` K ) )

Proof

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