Users' Mathboxes 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 29714
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 29712 . 2 class pstoMet
2 vd . . 3 setvar 𝑑
3 cpsmet 19649 . . . . 5 class PsMet
43crn 5075 . . . 4 class ran PsMet
54cuni 4402 . . 3 class ran PsMet
6 va . . . 4 setvar 𝑎
7 vb . . . 4 setvar 𝑏
82cv 1479 . . . . . . 7 class 𝑑
98cdm 5074 . . . . . 6 class dom 𝑑
109cdm 5074 . . . . 5 class dom dom 𝑑
11 cmetid 29711 . . . . . 6 class ~Met
128, 11cfv 5847 . . . . 5 class (~Met𝑑)
1310, 12cqs 7686 . . . 4 class (dom dom 𝑑 / (~Met𝑑))
14 vz . . . . . . . . . 10 setvar 𝑧
1514cv 1479 . . . . . . . . 9 class 𝑧
16 vx . . . . . . . . . . 11 setvar 𝑥
1716cv 1479 . . . . . . . . . 10 class 𝑥
18 vy . . . . . . . . . . 11 setvar 𝑦
1918cv 1479 . . . . . . . . . 10 class 𝑦
2017, 19, 8co 6604 . . . . . . . . 9 class (𝑥𝑑𝑦)
2115, 20wceq 1480 . . . . . . . 8 wff 𝑧 = (𝑥𝑑𝑦)
227cv 1479 . . . . . . . 8 class 𝑏
2321, 18, 22wrex 2908 . . . . . . 7 wff 𝑦𝑏 𝑧 = (𝑥𝑑𝑦)
246cv 1479 . . . . . . 7 class 𝑎
2523, 16, 24wrex 2908 . . . . . 6 wff 𝑥𝑎𝑦𝑏 𝑧 = (𝑥𝑑𝑦)
2625, 14cab 2607 . . . . 5 class {𝑧 ∣ ∃𝑥𝑎𝑦𝑏 𝑧 = (𝑥𝑑𝑦)}
2726cuni 4402 . . . 4 class {𝑧 ∣ ∃𝑥𝑎𝑦𝑏 𝑧 = (𝑥𝑑𝑦)}
286, 7, 13, 13, 27cmpt2 6606 . . 3 class (𝑎 ∈ (dom dom 𝑑 / (~Met𝑑)), 𝑏 ∈ (dom dom 𝑑 / (~Met𝑑)) ↦ {𝑧 ∣ ∃𝑥𝑎𝑦𝑏 𝑧 = (𝑥𝑑𝑦)})
292, 5, 28cmpt 4673 . 2 class (𝑑 ran PsMet ↦ (𝑎 ∈ (dom dom 𝑑 / (~Met𝑑)), 𝑏 ∈ (dom dom 𝑑 / (~Met𝑑)) ↦ {𝑧 ∣ ∃𝑥𝑎𝑦𝑏 𝑧 = (𝑥𝑑𝑦)}))
301, 29wceq 1480 1 wff pstoMet = (𝑑 ran PsMet ↦ (𝑎 ∈ (dom dom 𝑑 / (~Met𝑑)), 𝑏 ∈ (dom dom 𝑑 / (~Met𝑑)) ↦ {𝑧 ∣ ∃𝑥𝑎𝑦𝑏 𝑧 = (𝑥𝑑𝑦)}))
Colors of variables: wff setvar class
This definition is referenced by:  pstmval  29720
  Copyright terms: Public domain W3C validator