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 = { 𝑓 ∈ ∞MetSp ∣ ( ( dist ‘ 𝑓 ) ↾ ( ( Base ‘ 𝑓 ) × ( Base ‘ 𝑓 ) ) ) ∈ ( Met ‘ ( Base ‘ 𝑓 ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cms ⊢ MetSp
1 vf ⊢ 𝑓
2 cxms ⊢ ∞MetSp
3 cds ⊢ dist
4 1 cv ⊢ 𝑓
5 4 3 cfv ⊢ ( dist ‘ 𝑓 )
6 cbs ⊢ Base
7 4 6 cfv ⊢ ( Base ‘ 𝑓 )
8 7 7 cxp ⊢ ( ( Base ‘ 𝑓 ) × ( Base ‘ 𝑓 ) )
9 5 8 cres ⊢ ( ( dist ‘ 𝑓 ) ↾ ( ( Base ‘ 𝑓 ) × ( Base ‘ 𝑓 ) ) )
10 cmet ⊢ Met
11 7 10 cfv ⊢ ( Met ‘ ( Base ‘ 𝑓 ) )
12 9 11 wcel ⊢ ( ( dist ‘ 𝑓 ) ↾ ( ( Base ‘ 𝑓 ) × ( Base ‘ 𝑓 ) ) ) ∈ ( Met ‘ ( Base ‘ 𝑓 ) )
13 12 1 2 crab ⊢ { 𝑓 ∈ ∞MetSp ∣ ( ( dist ‘ 𝑓 ) ↾ ( ( Base ‘ 𝑓 ) × ( Base ‘ 𝑓 ) ) ) ∈ ( Met ‘ ( Base ‘ 𝑓 ) ) }
14 0 13 wceq ⊢ MetSp = { 𝑓 ∈ ∞MetSp ∣ ( ( dist ‘ 𝑓 ) ↾ ( ( Base ‘ 𝑓 ) × ( Base ‘ 𝑓 ) ) ) ∈ ( Met ‘ ( Base ‘ 𝑓 ) ) }