Metamath Proof Explorer

Definition df-pstm

Description: Define the metric induced by a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018)

Ref Expression
Assertion df-pstm ⊢ pstoMet = d ∈ ⋃ ran ⁡ PsMet ⟼ a ∈ dom ⁡ dom ⁡ d / ~ Met ⁡ d , b ∈ dom ⁡ dom ⁡ d / ~ Met ⁡ d ⟼ ⋃ z | ∃ x ∈ a ∃ y ∈ b z = x d y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpstm class pstoMet
1 vd setvar d
2 cpsmet class PsMet
3 2 crn class ran ⁡ PsMet
4 3 cuni class ⋃ ran ⁡ PsMet
5 va setvar a
6 1 cv setvar d
7 6 cdm class dom ⁡ d
8 7 cdm class dom ⁡ dom ⁡ d
9 cmetid class ~ Met
10 6 9 cfv class ~ Met ⁡ d
11 8 10 cqs class dom ⁡ dom ⁡ d / ~ Met ⁡ d
12 vb setvar b
13 vz setvar z
14 vx setvar x
15 5 cv setvar a
16 vy setvar y
17 12 cv setvar b
18 13 cv setvar z
19 14 cv setvar x
20 16 cv setvar y
21 19 20 6 co class x d y
22 18 21 wceq wff z = x d y
23 22 16 17 wrex wff ∃ y ∈ b z = x d y
24 23 14 15 wrex wff ∃ x ∈ a ∃ y ∈ b z = x d y
25 24 13 cab class z | ∃ x ∈ a ∃ y ∈ b z = x d y
26 25 cuni class ⋃ z | ∃ x ∈ a ∃ y ∈ b z = x d y
27 5 12 11 11 26 cmpo class a ∈ dom ⁡ dom ⁡ d / ~ Met ⁡ d , b ∈ dom ⁡ dom ⁡ d / ~ Met ⁡ d ⟼ ⋃ z | ∃ x ∈ a ∃ y ∈ b z = x d y
28 1 4 27 cmpt class d ∈ ⋃ ran ⁡ PsMet ⟼ a ∈ dom ⁡ dom ⁡ d / ~ Met ⁡ d , b ∈ dom ⁡ dom ⁡ d / ~ Met ⁡ d ⟼ ⋃ z | ∃ x ∈ a ∃ y ∈ b z = x d y
29 0 28 wceq wff pstoMet = d ∈ ⋃ ran ⁡ PsMet ⟼ a ∈ dom ⁡ dom ⁡ d / ~ Met ⁡ d , b ∈ dom ⁡ dom ⁡ d / ~ Met ⁡ d ⟼ ⋃ z | ∃ x ∈ a ∃ y ∈ b z = x d y