Metamath Proof Explorer


Theorem isms

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
Assertion isms K MetSp K ∞MetSp D Met X

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
4 fveq2 f = K dist f = dist K
5 fveq2 f = K Base f = Base K
6 5 2 eqtr4di f = K Base f = X
7 6 sqxpeqd f = K Base f × Base f = X × X
8 4 7 reseq12d f = K dist f Base f × Base f = dist K X × X
9 8 3 eqtr4di f = K dist f Base f × Base f = D
10 6 fveq2d f = K Met Base f = Met X
11 9 10 eleq12d f = K dist f Base f × Base f Met Base f D Met X
12 df-ms MetSp = f ∞MetSp | dist f Base f × Base f Met Base f
13 11 12 elrab2 K MetSp K ∞MetSp D Met X