Definition df-xmet

Description: Define the set of all extended metrics on a given base set. The definition is similar to df-met , but we also allow the metric to take on the value +oo . (Contributed by Mario Carneiro, 20-Aug-2015)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cxmet	⊢ ∞Met
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		vd	⊢ 𝑑
4		cxr	⊢ ℝ*
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		cxad	⊢ +𝑒
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 ↔ 𝑦 = 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑥 ( 𝑦 𝑑 𝑧 ) ≤ ( ( 𝑤 𝑑 𝑦 ) +𝑒 ( 𝑤 𝑑 𝑧 ) ) ) } )