Definition df-hcmp 31809

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 31808	. 2 class HCmp
2		vu	. . . . . . 7 setvar 𝑢
3	2	cv 1538	. . . . . 6 class 𝑢
4		cust 23259	. . . . . . . 8 class UnifOn
5	4	crn 5581	. . . . . . 7 class ran UnifOn
6	5	cuni 4836	. . . . . 6 class ∪ ran UnifOn
7	3, 6	wcel 2108	. . . . 5 wff 𝑢 ∈ ∪ ran UnifOn
8		vw	. . . . . . 7 setvar 𝑤
9	8	cv 1538	. . . . . 6 class 𝑤
10		ccusp 23357	. . . . . 6 class CUnifSp
11	9, 10	wcel 2108	. . . . 5 wff 𝑤 ∈ CUnifSp
12	7, 11	wa 395	. . . 4 wff (𝑢 ∈ ∪ ran UnifOn ∧ 𝑤 ∈ CUnifSp)
13		cuss 23313	. . . . . . 7 class UnifSt
14	9, 13	cfv 6418	. . . . . 6 class (UnifSt‘𝑤)
15	3	cuni 4836	. . . . . . 7 class ∪ 𝑢
16	15	cdm 5580	. . . . . 6 class dom ∪ 𝑢
17		crest 17048	. . . . . 6 class ↾t
18	14, 16, 17	co 7255	. . . . 5 class ((UnifSt‘𝑤) ↾t dom ∪ 𝑢)
19	18, 3	wceq 1539	. . . 4 wff ((UnifSt‘𝑤) ↾t dom ∪ 𝑢) = 𝑢
20		ctopn 17049	. . . . . . . 8 class TopOpen
21	9, 20	cfv 6418	. . . . . . 7 class (TopOpen‘𝑤)
22		ccl 22077	. . . . . . 7 class cls
23	21, 22	cfv 6418	. . . . . 6 class (cls‘(TopOpen‘𝑤))
24	16, 23	cfv 6418	. . . . 5 class ((cls‘(TopOpen‘𝑤))‘dom ∪ 𝑢)
25		cbs 16840	. . . . . 6 class Base
26	9, 25	cfv 6418	. . . . 5 class (Base‘𝑤)
27	24, 26	wceq 1539	. . . 4 wff ((cls‘(TopOpen‘𝑤))‘dom ∪ 𝑢) = (Base‘𝑤)
28	12, 19, 27	w3a 1085	. . 3 wff ((𝑢 ∈ ∪ ran UnifOn ∧ 𝑤 ∈ CUnifSp) ∧ ((UnifSt‘𝑤) ↾t dom ∪ 𝑢) = 𝑢 ∧ ((cls‘(TopOpen‘𝑤))‘dom ∪ 𝑢) = (Base‘𝑤))
29	28, 2, 8	copab 5132	. 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)