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 ‘ 𝑓 ) ) }