This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-ms

Description: Define the (proper) class of metric spaces. (Contributed by NM, 27-Aug-2006)

Ref Expression
Assertion df-ms ⊢ MetSp = f ∈ ∞MetSp | dist ⁡ f ↾ Base f × Base f ∈ Met ⁡ Base f

Detailed syntax breakdown

Step Hyp Ref Expression
0 cms class MetSp
1 vf setvar f
2 cxms class ∞MetSp
3 cds class dist
4 1 cv setvar f
5 4 3 cfv class dist ⁡ f
6 cbs class Base
7 4 6 cfv class Base f
8 7 7 cxp class Base f × Base f
9 5 8 cres class dist ⁡ f ↾ Base f × Base f
10 cmet class Met
11 7 10 cfv class Met ⁡ Base f
12 9 11 wcel wff dist ⁡ f ↾ Base f × Base f ∈ Met ⁡ Base f
13 12 1 2 crab class f ∈ ∞MetSp | dist ⁡ f ↾ Base f × Base f ∈ Met ⁡ Base f
14 0 13 wceq wff MetSp = f ∈ ∞MetSp | dist ⁡ f ↾ Base f × Base f ∈ Met ⁡ Base f