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 29331
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 unicity 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 29330 . 2 class HCmp
2 vu . . . . . . 7 setvar 𝑢
32cv 1474 . . . . . 6 class 𝑢
4 cust 21813 . . . . . . . 8 class UnifOn
54crn 5039 . . . . . . 7 class ran UnifOn
65cuni 4372 . . . . . 6 class ran UnifOn
73, 6wcel 1977 . . . . 5 wff 𝑢 ran UnifOn
8 vw . . . . . . 7 setvar 𝑤
98cv 1474 . . . . . 6 class 𝑤
10 ccusp 21911 . . . . . 6 class CUnifSp
119, 10wcel 1977 . . . . 5 wff 𝑤 ∈ CUnifSp
127, 11wa 383 . . . 4 wff (𝑢 ran UnifOn ∧ 𝑤 ∈ CUnifSp)
13 cuss 21867 . . . . . . 7 class UnifSt
149, 13cfv 5804 . . . . . 6 class (UnifSt‘𝑤)
153cuni 4372 . . . . . . 7 class 𝑢
1615cdm 5038 . . . . . 6 class dom 𝑢
17 crest 15904 . . . . . 6 class t
1814, 16, 17co 6549 . . . . 5 class ((UnifSt‘𝑤) ↾t dom 𝑢)
1918, 3wceq 1475 . . . 4 wff ((UnifSt‘𝑤) ↾t dom 𝑢) = 𝑢
20 ctopn 15905 . . . . . . . 8 class TopOpen
219, 20cfv 5804 . . . . . . 7 class (TopOpen‘𝑤)
22 ccl 20632 . . . . . . 7 class cls
2321, 22cfv 5804 . . . . . 6 class (cls‘(TopOpen‘𝑤))
2416, 23cfv 5804 . . . . 5 class ((cls‘(TopOpen‘𝑤))‘dom 𝑢)
25 cbs 15695 . . . . . 6 class Base
269, 25cfv 5804 . . . . 5 class (Base‘𝑤)
2724, 26wceq 1475 . . . 4 wff ((cls‘(TopOpen‘𝑤))‘dom 𝑢) = (Base‘𝑤)
2812, 19, 27w3a 1031 . . 3 wff ((𝑢 ran UnifOn ∧ 𝑤 ∈ CUnifSp) ∧ ((UnifSt‘𝑤) ↾t dom 𝑢) = 𝑢 ∧ ((cls‘(TopOpen‘𝑤))‘dom 𝑢) = (Base‘𝑤))
2928, 2, 8copab 4642 . 2 class {⟨𝑢, 𝑤⟩ ∣ ((𝑢 ran UnifOn ∧ 𝑤 ∈ CUnifSp) ∧ ((UnifSt‘𝑤) ↾t dom 𝑢) = 𝑢 ∧ ((cls‘(TopOpen‘𝑤))‘dom 𝑢) = (Base‘𝑤))}
301, 29wceq 1475 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