Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-pstm Structured version   Visualization version   GIF version

Definition df-pstm 30272
 Description: Define the metric induced by a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.)
Assertion
Ref Expression
df-pstm pstoMet = (𝑑 ran PsMet ↦ (𝑎 ∈ (dom dom 𝑑 / (~Met𝑑)), 𝑏 ∈ (dom dom 𝑑 / (~Met𝑑)) ↦ {𝑧 ∣ ∃𝑥𝑎𝑦𝑏 𝑧 = (𝑥𝑑𝑦)}))
Distinct variable group:   𝑎,𝑏,𝑑,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-pstm
StepHypRef Expression
1 cpstm 30270 . 2 class pstoMet
2 vd . . 3 setvar 𝑑
3 cpsmet 19945 . . . . 5 class PsMet
43crn 5250 . . . 4 class ran PsMet
54cuni 4574 . . 3 class ran PsMet
6 va . . . 4 setvar 𝑎
7 vb . . . 4 setvar 𝑏
82cv 1630 . . . . . . 7 class 𝑑
98cdm 5249 . . . . . 6 class dom 𝑑
109cdm 5249 . . . . 5 class dom dom 𝑑
11 cmetid 30269 . . . . . 6 class ~Met
128, 11cfv 6031 . . . . 5 class (~Met𝑑)
1310, 12cqs 7895 . . . 4 class (dom dom 𝑑 / (~Met𝑑))
14 vz . . . . . . . . . 10 setvar 𝑧
1514cv 1630 . . . . . . . . 9 class 𝑧
16 vx . . . . . . . . . . 11 setvar 𝑥
1716cv 1630 . . . . . . . . . 10 class 𝑥
18 vy . . . . . . . . . . 11 setvar 𝑦
1918cv 1630 . . . . . . . . . 10 class 𝑦
2017, 19, 8co 6793 . . . . . . . . 9 class (𝑥𝑑𝑦)
2115, 20wceq 1631 . . . . . . . 8 wff 𝑧 = (𝑥𝑑𝑦)
227cv 1630 . . . . . . . 8 class 𝑏
2321, 18, 22wrex 3062 . . . . . . 7 wff 𝑦𝑏 𝑧 = (𝑥𝑑𝑦)
246cv 1630 . . . . . . 7 class 𝑎
2523, 16, 24wrex 3062 . . . . . 6 wff 𝑥𝑎𝑦𝑏 𝑧 = (𝑥𝑑𝑦)
2625, 14cab 2757 . . . . 5 class {𝑧 ∣ ∃𝑥𝑎𝑦𝑏 𝑧 = (𝑥𝑑𝑦)}
2726cuni 4574 . . . 4 class {𝑧 ∣ ∃𝑥𝑎𝑦𝑏 𝑧 = (𝑥𝑑𝑦)}
286, 7, 13, 13, 27cmpt2 6795 . . 3 class (𝑎 ∈ (dom dom 𝑑 / (~Met𝑑)), 𝑏 ∈ (dom dom 𝑑 / (~Met𝑑)) ↦ {𝑧 ∣ ∃𝑥𝑎𝑦𝑏 𝑧 = (𝑥𝑑𝑦)})
292, 5, 28cmpt 4863 . 2 class (𝑑 ran PsMet ↦ (𝑎 ∈ (dom dom 𝑑 / (~Met𝑑)), 𝑏 ∈ (dom dom 𝑑 / (~Met𝑑)) ↦ {𝑧 ∣ ∃𝑥𝑎𝑦𝑏 𝑧 = (𝑥𝑑𝑦)}))
301, 29wceq 1631 1 wff pstoMet = (𝑑 ran PsMet ↦ (𝑎 ∈ (dom dom 𝑑 / (~Met𝑑)), 𝑏 ∈ (dom dom 𝑑 / (~Met𝑑)) ↦ {𝑧 ∣ ∃𝑥𝑎𝑦𝑏 𝑧 = (𝑥𝑑𝑦)}))
 Colors of variables: wff setvar class This definition is referenced by:  pstmval  30278
 Copyright terms: Public domain W3C validator