# Metamath Proof Explorer

## Definition df-hcmp

Description: Definition of the Hausdorff completion. In this definition, a structure w is a Hausdorff completion of a uniform structure u if w is a complete uniform space, in which u 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)

Ref Expression
Assertion df-hcmp ${⊢}\mathrm{HCmp}=\left\{⟨{u},{w}⟩|\left(\left({u}\in \bigcup \mathrm{ran}\mathrm{UnifOn}\wedge {w}\in \mathrm{CUnifSp}\right)\wedge \mathrm{UnifSt}\left({w}\right){↾}_{𝑡}\mathrm{dom}\bigcup {u}={u}\wedge \mathrm{cls}\left(\mathrm{TopOpen}\left({w}\right)\right)\left(\mathrm{dom}\bigcup {u}\right)={\mathrm{Base}}_{{w}}\right)\right\}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 chcmp ${class}\mathrm{HCmp}$
1 vu ${setvar}{u}$
2 vw ${setvar}{w}$
3 1 cv ${setvar}{u}$
4 cust ${class}\mathrm{UnifOn}$
5 4 crn ${class}\mathrm{ran}\mathrm{UnifOn}$
6 5 cuni ${class}\bigcup \mathrm{ran}\mathrm{UnifOn}$
7 3 6 wcel ${wff}{u}\in \bigcup \mathrm{ran}\mathrm{UnifOn}$
8 2 cv ${setvar}{w}$
9 ccusp ${class}\mathrm{CUnifSp}$
10 8 9 wcel ${wff}{w}\in \mathrm{CUnifSp}$
11 7 10 wa ${wff}\left({u}\in \bigcup \mathrm{ran}\mathrm{UnifOn}\wedge {w}\in \mathrm{CUnifSp}\right)$
12 cuss ${class}\mathrm{UnifSt}$
13 8 12 cfv ${class}\mathrm{UnifSt}\left({w}\right)$
14 crest ${class}{↾}_{𝑡}$
15 3 cuni ${class}\bigcup {u}$
16 15 cdm ${class}\mathrm{dom}\bigcup {u}$
17 13 16 14 co ${class}\left(\mathrm{UnifSt}\left({w}\right){↾}_{𝑡}\mathrm{dom}\bigcup {u}\right)$
18 17 3 wceq ${wff}\mathrm{UnifSt}\left({w}\right){↾}_{𝑡}\mathrm{dom}\bigcup {u}={u}$
19 ccl ${class}\mathrm{cls}$
20 ctopn ${class}\mathrm{TopOpen}$
21 8 20 cfv ${class}\mathrm{TopOpen}\left({w}\right)$
22 21 19 cfv ${class}\mathrm{cls}\left(\mathrm{TopOpen}\left({w}\right)\right)$
23 16 22 cfv ${class}\mathrm{cls}\left(\mathrm{TopOpen}\left({w}\right)\right)\left(\mathrm{dom}\bigcup {u}\right)$
24 cbs ${class}\mathrm{Base}$
25 8 24 cfv ${class}{\mathrm{Base}}_{{w}}$
26 23 25 wceq ${wff}\mathrm{cls}\left(\mathrm{TopOpen}\left({w}\right)\right)\left(\mathrm{dom}\bigcup {u}\right)={\mathrm{Base}}_{{w}}$
27 11 18 26 w3a ${wff}\left(\left({u}\in \bigcup \mathrm{ran}\mathrm{UnifOn}\wedge {w}\in \mathrm{CUnifSp}\right)\wedge \mathrm{UnifSt}\left({w}\right){↾}_{𝑡}\mathrm{dom}\bigcup {u}={u}\wedge \mathrm{cls}\left(\mathrm{TopOpen}\left({w}\right)\right)\left(\mathrm{dom}\bigcup {u}\right)={\mathrm{Base}}_{{w}}\right)$
28 27 1 2 copab ${class}\left\{⟨{u},{w}⟩|\left(\left({u}\in \bigcup \mathrm{ran}\mathrm{UnifOn}\wedge {w}\in \mathrm{CUnifSp}\right)\wedge \mathrm{UnifSt}\left({w}\right){↾}_{𝑡}\mathrm{dom}\bigcup {u}={u}\wedge \mathrm{cls}\left(\mathrm{TopOpen}\left({w}\right)\right)\left(\mathrm{dom}\bigcup {u}\right)={\mathrm{Base}}_{{w}}\right)\right\}$
29 0 28 wceq ${wff}\mathrm{HCmp}=\left\{⟨{u},{w}⟩|\left(\left({u}\in \bigcup \mathrm{ran}\mathrm{UnifOn}\wedge {w}\in \mathrm{CUnifSp}\right)\wedge \mathrm{UnifSt}\left({w}\right){↾}_{𝑡}\mathrm{dom}\bigcup {u}={u}\wedge \mathrm{cls}\left(\mathrm{TopOpen}\left({w}\right)\right)\left(\mathrm{dom}\bigcup {u}\right)={\mathrm{Base}}_{{w}}\right)\right\}$