Metamath Proof Explorer


Theorem isxms

Description: Express the predicate " <. X , D >. is an extended metric space" with underlying set X and distance function D . (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses isms.j J=TopOpenK
isms.x X=BaseK
isms.d D=distKX×X
Assertion isxms K∞MetSpKTopSpJ=MetOpenD

Proof

Step Hyp Ref Expression
1 isms.j J=TopOpenK
2 isms.x X=BaseK
3 isms.d D=distKX×X
4 fveq2 f=KTopOpenf=TopOpenK
5 4 1 eqtr4di f=KTopOpenf=J
6 fveq2 f=Kdistf=distK
7 fveq2 f=KBasef=BaseK
8 7 2 eqtr4di f=KBasef=X
9 8 sqxpeqd f=KBasef×Basef=X×X
10 6 9 reseq12d f=KdistfBasef×Basef=distKX×X
11 10 3 eqtr4di f=KdistfBasef×Basef=D
12 11 fveq2d f=KMetOpendistfBasef×Basef=MetOpenD
13 5 12 eqeq12d f=KTopOpenf=MetOpendistfBasef×BasefJ=MetOpenD
14 df-xms ∞MetSp=fTopSp|TopOpenf=MetOpendistfBasef×Basef
15 13 14 elrab2 K∞MetSpKTopSpJ=MetOpenD