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 31274
 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 31273 . 2 class HCmp
2 vu . . . . . . 7 setvar 𝑢
32cv 1537 . . . . . 6 class 𝑢
4 cust 22803 . . . . . . . 8 class UnifOn
54crn 5533 . . . . . . 7 class ran UnifOn
65cuni 4813 . . . . . 6 class ran UnifOn
73, 6wcel 2114 . . . . 5 wff 𝑢 ran UnifOn
8 vw . . . . . . 7 setvar 𝑤
98cv 1537 . . . . . 6 class 𝑤
10 ccusp 22901 . . . . . 6 class CUnifSp
119, 10wcel 2114 . . . . 5 wff 𝑤 ∈ CUnifSp
127, 11wa 399 . . . 4 wff (𝑢 ran UnifOn ∧ 𝑤 ∈ CUnifSp)
13 cuss 22857 . . . . . . 7 class UnifSt
149, 13cfv 6334 . . . . . 6 class (UnifSt‘𝑤)
153cuni 4813 . . . . . . 7 class 𝑢
1615cdm 5532 . . . . . 6 class dom 𝑢
17 crest 16685 . . . . . 6 class t
1814, 16, 17co 7140 . . . . 5 class ((UnifSt‘𝑤) ↾t dom 𝑢)
1918, 3wceq 1538 . . . 4 wff ((UnifSt‘𝑤) ↾t dom 𝑢) = 𝑢
20 ctopn 16686 . . . . . . . 8 class TopOpen
219, 20cfv 6334 . . . . . . 7 class (TopOpen‘𝑤)
22 ccl 21621 . . . . . . 7 class cls
2321, 22cfv 6334 . . . . . 6 class (cls‘(TopOpen‘𝑤))
2416, 23cfv 6334 . . . . 5 class ((cls‘(TopOpen‘𝑤))‘dom 𝑢)
25 cbs 16474 . . . . . 6 class Base
269, 25cfv 6334 . . . . 5 class (Base‘𝑤)
2724, 26wceq 1538 . . . 4 wff ((cls‘(TopOpen‘𝑤))‘dom 𝑢) = (Base‘𝑤)
2812, 19, 27w3a 1084 . . 3 wff ((𝑢 ran UnifOn ∧ 𝑤 ∈ CUnifSp) ∧ ((UnifSt‘𝑤) ↾t dom 𝑢) = 𝑢 ∧ ((cls‘(TopOpen‘𝑤))‘dom 𝑢) = (Base‘𝑤))
2928, 2, 8copab 5104 . 2 class {⟨𝑢, 𝑤⟩ ∣ ((𝑢 ran UnifOn ∧ 𝑤 ∈ CUnifSp) ∧ ((UnifSt‘𝑤) ↾t dom 𝑢) = 𝑢 ∧ ((cls‘(TopOpen‘𝑤))‘dom 𝑢) = (Base‘𝑤))}
301, 29wceq 1538 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