Definition df-met

Description: Define the (proper) class of all metrics. (A metric space is the metric's base set paired with the metric; see df-ms . However, we will often also call the metric itself a "metric space".) Equivalent to Definition 14-1.1 of Gleason p. 223. The 4 properties in Gleason's definition are shown by met0 , metgt0 , metsym , and mettri . (Contributed by NM, 25-Aug-2006)

	Ref	Expression
Assertion	df-met	⊢ Met = ( 𝑥 ∈ V ↦ { 𝑑 ∈ ( ℝ ↑m ( 𝑥 × 𝑥 ) ) ∣ ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( ( ( 𝑦 𝑑 𝑧 ) = 0 ↔ 𝑦 = 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑥 ( 𝑦 𝑑 𝑧 ) ≤ ( ( 𝑤 𝑑 𝑦 ) + ( 𝑤 𝑑 𝑧 ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmet	⊢ Met
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		vd	⊢ 𝑑
4		cr	⊢ ℝ
5		cmap	⊢ ↑m
6	1	cv	⊢ 𝑥
7	6 6	cxp	⊢ ( 𝑥 × 𝑥 )
8	4 7 5	co	⊢ ( ℝ ↑m ( 𝑥 × 𝑥 ) )
9		vy	⊢ 𝑦
10		vz	⊢ 𝑧
11	9	cv	⊢ 𝑦
12	3	cv	⊢ 𝑑
13	10	cv	⊢ 𝑧
14	11 13 12	co	⊢ ( 𝑦 𝑑 𝑧 )
15		cc0	⊢ 0
16	14 15	wceq	⊢ ( 𝑦 𝑑 𝑧 ) = 0
17	11 13	wceq	⊢ 𝑦 = 𝑧
18	16 17	wb	⊢ ( ( 𝑦 𝑑 𝑧 ) = 0 ↔ 𝑦 = 𝑧 )
19		vw	⊢ 𝑤
20		cle	⊢ ≤
21	19	cv	⊢ 𝑤
22	21 11 12	co	⊢ ( 𝑤 𝑑 𝑦 )
23		caddc	⊢ +
24	21 13 12	co	⊢ ( 𝑤 𝑑 𝑧 )
25	22 24 23	co	⊢ ( ( 𝑤 𝑑 𝑦 ) + ( 𝑤 𝑑 𝑧 ) )
26	14 25 20	wbr	⊢ ( 𝑦 𝑑 𝑧 ) ≤ ( ( 𝑤 𝑑 𝑦 ) + ( 𝑤 𝑑 𝑧 ) )
27	26 19 6	wral	⊢ ∀ 𝑤 ∈ 𝑥 ( 𝑦 𝑑 𝑧 ) ≤ ( ( 𝑤 𝑑 𝑦 ) + ( 𝑤 𝑑 𝑧 ) )
28	18 27	wa	⊢ ( ( ( 𝑦 𝑑 𝑧 ) = 0 ↔ 𝑦 = 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑥 ( 𝑦 𝑑 𝑧 ) ≤ ( ( 𝑤 𝑑 𝑦 ) + ( 𝑤 𝑑 𝑧 ) ) )
29	28 10 6	wral	⊢ ∀ 𝑧 ∈ 𝑥 ( ( ( 𝑦 𝑑 𝑧 ) = 0 ↔ 𝑦 = 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑥 ( 𝑦 𝑑 𝑧 ) ≤ ( ( 𝑤 𝑑 𝑦 ) + ( 𝑤 𝑑 𝑧 ) ) )
30	29 9 6	wral	⊢ ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( ( ( 𝑦 𝑑 𝑧 ) = 0 ↔ 𝑦 = 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑥 ( 𝑦 𝑑 𝑧 ) ≤ ( ( 𝑤 𝑑 𝑦 ) + ( 𝑤 𝑑 𝑧 ) ) )
31	30 3 8	crab	⊢ { 𝑑 ∈ ( ℝ ↑m ( 𝑥 × 𝑥 ) ) ∣ ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( ( ( 𝑦 𝑑 𝑧 ) = 0 ↔ 𝑦 = 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑥 ( 𝑦 𝑑 𝑧 ) ≤ ( ( 𝑤 𝑑 𝑦 ) + ( 𝑤 𝑑 𝑧 ) ) ) }
32	1 2 31	cmpt	⊢ ( 𝑥 ∈ V ↦ { 𝑑 ∈ ( ℝ ↑m ( 𝑥 × 𝑥 ) ) ∣ ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( ( ( 𝑦 𝑑 𝑧 ) = 0 ↔ 𝑦 = 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑥 ( 𝑦 𝑑 𝑧 ) ≤ ( ( 𝑤 𝑑 𝑦 ) + ( 𝑤 𝑑 𝑧 ) ) ) } )
33	0 32	wceq	⊢ Met = ( 𝑥 ∈ V ↦ { 𝑑 ∈ ( ℝ ↑m ( 𝑥 × 𝑥 ) ) ∣ ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( ( ( 𝑦 𝑑 𝑧 ) = 0 ↔ 𝑦 = 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑥 ( 𝑦 𝑑 𝑧 ) ≤ ( ( 𝑤 𝑑 𝑦 ) + ( 𝑤 𝑑 𝑧 ) ) ) } )