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

Definition df-hcmp 31099
Description: Definition of the Hausdorff completion. In this definition, a structure 𝑤 is a Hausdorff completion of a uniform structure 𝑢 if 𝑤 is a complete uniform space, in which 𝑢 is dense, and which admits the same uniform structure. Theorem 3 of [BourbakiTop1] p. II.21. states the existence and uniqueness of such a completion. (Contributed by Thierry Arnoux, 5-Mar-2018.)
Assertion
Ref Expression
df-hcmp HCmp = {⟨𝑢, 𝑤⟩ ∣ ((𝑢 ran UnifOn ∧ 𝑤 ∈ CUnifSp) ∧ ((UnifSt‘𝑤) ↾t dom 𝑢) = 𝑢 ∧ ((cls‘(TopOpen‘𝑤))‘dom 𝑢) = (Base‘𝑤))}
Distinct variable group:   𝑤,𝑢

Detailed syntax breakdown of Definition df-hcmp
StepHypRef Expression
1 chcmp 31098 . 2 class HCmp
2 vu . . . . . . 7 setvar 𝑢
32cv 1527 . . . . . 6 class 𝑢
4 cust 22735 . . . . . . . 8 class UnifOn
54crn 5549 . . . . . . 7 class ran UnifOn
65cuni 4830 . . . . . 6 class ran UnifOn
73, 6wcel 2105 . . . . 5 wff 𝑢 ran UnifOn
8 vw . . . . . . 7 setvar 𝑤
98cv 1527 . . . . . 6 class 𝑤
10 ccusp 22833 . . . . . 6 class CUnifSp
119, 10wcel 2105 . . . . 5 wff 𝑤 ∈ CUnifSp
127, 11wa 396 . . . 4 wff (𝑢 ran UnifOn ∧ 𝑤 ∈ CUnifSp)
13 cuss 22789 . . . . . . 7 class UnifSt
149, 13cfv 6348 . . . . . 6 class (UnifSt‘𝑤)
153cuni 4830 . . . . . . 7 class 𝑢
1615cdm 5548 . . . . . 6 class dom 𝑢
17 crest 16682 . . . . . 6 class t
1814, 16, 17co 7145 . . . . 5 class ((UnifSt‘𝑤) ↾t dom 𝑢)
1918, 3wceq 1528 . . . 4 wff ((UnifSt‘𝑤) ↾t dom 𝑢) = 𝑢
20 ctopn 16683 . . . . . . . 8 class TopOpen
219, 20cfv 6348 . . . . . . 7 class (TopOpen‘𝑤)
22 ccl 21554 . . . . . . 7 class cls
2321, 22cfv 6348 . . . . . 6 class (cls‘(TopOpen‘𝑤))
2416, 23cfv 6348 . . . . 5 class ((cls‘(TopOpen‘𝑤))‘dom 𝑢)
25 cbs 16471 . . . . . 6 class Base
269, 25cfv 6348 . . . . 5 class (Base‘𝑤)
2724, 26wceq 1528 . . . 4 wff ((cls‘(TopOpen‘𝑤))‘dom 𝑢) = (Base‘𝑤)
2812, 19, 27w3a 1079 . . 3 wff ((𝑢 ran UnifOn ∧ 𝑤 ∈ CUnifSp) ∧ ((UnifSt‘𝑤) ↾t dom 𝑢) = 𝑢 ∧ ((cls‘(TopOpen‘𝑤))‘dom 𝑢) = (Base‘𝑤))
2928, 2, 8copab 5119 . 2 class {⟨𝑢, 𝑤⟩ ∣ ((𝑢 ran UnifOn ∧ 𝑤 ∈ CUnifSp) ∧ ((UnifSt‘𝑤) ↾t dom 𝑢) = 𝑢 ∧ ((cls‘(TopOpen‘𝑤))‘dom 𝑢) = (Base‘𝑤))}
301, 29wceq 1528 1 wff HCmp = {⟨𝑢, 𝑤⟩ ∣ ((𝑢 ran UnifOn ∧ 𝑤 ∈ CUnifSp) ∧ ((UnifSt‘𝑤) ↾t dom 𝑢) = 𝑢 ∧ ((cls‘(TopOpen‘𝑤))‘dom 𝑢) = (Base‘𝑤))}
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator