Definition df-psmet

Description: Define the set of all pseudometrics on a given base set. In a pseudo metric, two distinct points may have a distance zero. (Contributed by Thierry Arnoux, 7-Feb-2018)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpsmet	⊢ PsMet
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	9	cv	⊢ 𝑦
11	3	cv	⊢ 𝑑
12	10 10 11	co	⊢ ( 𝑦 𝑑 𝑦 )
13		cc0	⊢ 0
14	12 13	wceq	⊢ ( 𝑦 𝑑 𝑦 ) = 0
15		vz	⊢ 𝑧
16		vw	⊢ 𝑤
17	15	cv	⊢ 𝑧
18	10 17 11	co	⊢ ( 𝑦 𝑑 𝑧 )
19		cle	⊢ ≤
20	16	cv	⊢ 𝑤
21	20 10 11	co	⊢ ( 𝑤 𝑑 𝑦 )
22		cxad	⊢ +e
23	20 17 11	co	⊢ ( 𝑤 𝑑 𝑧 )
24	21 23 22	co	⊢ ( ( 𝑤 𝑑 𝑦 ) +e ( 𝑤 𝑑 𝑧 ) )
25	18 24 19	wbr	⊢ ( 𝑦 𝑑 𝑧 ) ≤ ( ( 𝑤 𝑑 𝑦 ) +e ( 𝑤 𝑑 𝑧 ) )
26	25 16 6	wral	⊢ ∀ 𝑤 ∈ 𝑥 ( 𝑦 𝑑 𝑧 ) ≤ ( ( 𝑤 𝑑 𝑦 ) +e ( 𝑤 𝑑 𝑧 ) )
27	26 15 6	wral	⊢ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑦 𝑑 𝑧 ) ≤ ( ( 𝑤 𝑑 𝑦 ) +e ( 𝑤 𝑑 𝑧 ) )
28	14 27	wa	⊢ ( ( 𝑦 𝑑 𝑦 ) = 0 ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑦 𝑑 𝑧 ) ≤ ( ( 𝑤 𝑑 𝑦 ) +e ( 𝑤 𝑑 𝑧 ) ) )
29	28 9 6	wral	⊢ ∀ 𝑦 ∈ 𝑥 ( ( 𝑦 𝑑 𝑦 ) = 0 ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑦 𝑑 𝑧 ) ≤ ( ( 𝑤 𝑑 𝑦 ) +e ( 𝑤 𝑑 𝑧 ) ) )
30	29 3 8	crab	⊢ { 𝑑 ∈ ( ℝ* ↑m ( 𝑥 × 𝑥 ) ) ∣ ∀ 𝑦 ∈ 𝑥 ( ( 𝑦 𝑑 𝑦 ) = 0 ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑦 𝑑 𝑧 ) ≤ ( ( 𝑤 𝑑 𝑦 ) +e ( 𝑤 𝑑 𝑧 ) ) ) }
31	1 2 30	cmpt	⊢ ( 𝑥 ∈ V ↦ { 𝑑 ∈ ( ℝ* ↑m ( 𝑥 × 𝑥 ) ) ∣ ∀ 𝑦 ∈ 𝑥 ( ( 𝑦 𝑑 𝑦 ) = 0 ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑦 𝑑 𝑧 ) ≤ ( ( 𝑤 𝑑 𝑦 ) +e ( 𝑤 𝑑 𝑧 ) ) ) } )
32	0 31	wceq	⊢ PsMet = ( 𝑥 ∈ V ↦ { 𝑑 ∈ ( ℝ* ↑m ( 𝑥 × 𝑥 ) ) ∣ ∀ 𝑦 ∈ 𝑥 ( ( 𝑦 𝑑 𝑦 ) = 0 ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑦 𝑑 𝑧 ) ≤ ( ( 𝑤 𝑑 𝑦 ) +e ( 𝑤 𝑑 𝑧 ) ) ) } )