Definition df-hcmp 31907

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

Step	Hyp	Ref	Expression
1		chcmp 31906	. 2 class HCmp
2		vu	. . . . . . 7 setvar 𝑢
3	2	cv 1538	. . . . . 6 class 𝑢
4		cust 23351	. . . . . . . 8 class UnifOn
5	4	crn 5590	. . . . . . 7 class ran UnifOn
6	5	cuni 4839	. . . . . 6 class ∪ ran UnifOn
7	3, 6	wcel 2106	. . . . 5 wff 𝑢 ∈ ∪ ran UnifOn
8		vw	. . . . . . 7 setvar 𝑤
9	8	cv 1538	. . . . . 6 class 𝑤
10		ccusp 23449	. . . . . 6 class CUnifSp
11	9, 10	wcel 2106	. . . . 5 wff 𝑤 ∈ CUnifSp
12	7, 11	wa 396	. . . 4 wff (𝑢 ∈ ∪ ran UnifOn ∧ 𝑤 ∈ CUnifSp)
13		cuss 23405	. . . . . . 7 class UnifSt
14	9, 13	cfv 6433	. . . . . 6 class (UnifSt‘𝑤)
15	3	cuni 4839	. . . . . . 7 class ∪ 𝑢
16	15	cdm 5589	. . . . . 6 class dom ∪ 𝑢
17		crest 17131	. . . . . 6 class ↾t
18	14, 16, 17	co 7275	. . . . 5 class ((UnifSt‘𝑤) ↾t dom ∪ 𝑢)
19	18, 3	wceq 1539	. . . 4 wff ((UnifSt‘𝑤) ↾t dom ∪ 𝑢) = 𝑢
20		ctopn 17132	. . . . . . . 8 class TopOpen
21	9, 20	cfv 6433	. . . . . . 7 class (TopOpen‘𝑤)
22		ccl 22169	. . . . . . 7 class cls
23	21, 22	cfv 6433	. . . . . 6 class (cls‘(TopOpen‘𝑤))
24	16, 23	cfv 6433	. . . . 5 class ((cls‘(TopOpen‘𝑤))‘dom ∪ 𝑢)
25		cbs 16912	. . . . . 6 class Base
26	9, 25	cfv 6433	. . . . 5 class (Base‘𝑤)
27	24, 26	wceq 1539	. . . 4 wff ((cls‘(TopOpen‘𝑤))‘dom ∪ 𝑢) = (Base‘𝑤)
28	12, 19, 27	w3a 1086	. . 3 wff ((𝑢 ∈ ∪ ran UnifOn ∧ 𝑤 ∈ CUnifSp) ∧ ((UnifSt‘𝑤) ↾t dom ∪ 𝑢) = 𝑢 ∧ ((cls‘(TopOpen‘𝑤))‘dom ∪ 𝑢) = (Base‘𝑤))
29	28, 2, 8	copab 5136	. 2 class {⟨𝑢, 𝑤⟩ ∣ ((𝑢 ∈ ∪ ran UnifOn ∧ 𝑤 ∈ CUnifSp) ∧ ((UnifSt‘𝑤) ↾t dom ∪ 𝑢) = 𝑢 ∧ ((cls‘(TopOpen‘𝑤))‘dom ∪ 𝑢) = (Base‘𝑤))}
30	1, 29	wceq 1539	1 wff HCmp = {⟨𝑢, 𝑤⟩ ∣ ((𝑢 ∈ ∪ ran UnifOn ∧ 𝑤 ∈ CUnifSp) ∧ ((UnifSt‘𝑤) ↾t dom ∪ 𝑢) = 𝑢 ∧ ((cls‘(TopOpen‘𝑤))‘dom ∪ 𝑢) = (Base‘𝑤))}

This definition is referenced by: (None)