Theorem isms2

Description: Express the predicate " <. X , D >. is a metric space" with underlying set X and distance function D . (Contributed by NM, 27-Aug-2006) (Revised by Mario Carneiro, 24-Aug-2015)

	Ref	Expression
Hypotheses	isms.j	|- J = ( TopOpen ` K )
	isms.x	|- X = ( Base ` K )
	isms.d	|- D = ( ( dist ` K ) |` ( X X. X ) )
Assertion	isms2	|- ( K e. MetSp <-> ( D e. ( Met ` X ) /\ J = ( MetOpen ` D ) ) )

Proof

Step	Hyp	Ref	Expression
1		isms.j	|- J = ( TopOpen ` K )
2		isms.x	|- X = ( Base ` K )
3		isms.d	|- D = ( ( dist ` K ) |` ( X X. X ) )
4	1 2 3	isxms2	|- ( K e. *MetSp <-> ( D e. ( *Met ` X ) /\ J = ( MetOpen ` D ) ) )
5	4	anbi1i	|- ( ( K e. *MetSp /\ D e. ( Met ` X ) ) <-> ( ( D e. ( *Met ` X ) /\ J = ( MetOpen ` D ) ) /\ D e. ( Met ` X ) ) )
6	1 2 3	isms	|- ( K e. MetSp <-> ( K e. *MetSp /\ D e. ( Met ` X ) ) )
7		metxmet	|- ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
8	7	pm4.71ri	|- ( D e. ( Met ` X ) <-> ( D e. ( *Met ` X ) /\ D e. ( Met ` X ) ) )
9	8	anbi1i	|- ( ( D e. ( Met ` X ) /\ J = ( MetOpen ` D ) ) <-> ( ( D e. ( *Met ` X ) /\ D e. ( Met ` X ) ) /\ J = ( MetOpen ` D ) ) )
10		an32	|- ( ( ( D e. ( *Met ` X ) /\ D e. ( Met ` X ) ) /\ J = ( MetOpen ` D ) ) <-> ( ( D e. ( *Met ` X ) /\ J = ( MetOpen ` D ) ) /\ D e. ( Met ` X ) ) )
11	9 10	bitri	|- ( ( D e. ( Met ` X ) /\ J = ( MetOpen ` D ) ) <-> ( ( D e. ( *Met ` X ) /\ J = ( MetOpen ` D ) ) /\ D e. ( Met ` X ) ) )
12	5 6 11	3bitr4i	|- ( K e. MetSp <-> ( D e. ( Met ` X ) /\ J = ( MetOpen ` D ) ) )