Definition df-hcmp 34635

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 34634	. 2 class HCmp
2		vu	. . . . . . 7 setvar 𝑢
3	2	cv 1568	. . . . . 6 class 𝑢
4		cust 24524	. . . . . . . 8 class UnifOn
5	4	crn 5651	. . . . . . 7 class ran UnifOn
6	5	cuni 4866	. . . . . 6 class ∪ ran UnifOn
7	3, 6	wcel 2144	. . . . 5 wff 𝑢 ∈ ∪ ran UnifOn
8		vw	. . . . . . 7 setvar 𝑤
9	8	cv 1568	. . . . . 6 class 𝑤
10		ccusp 24620	. . . . . 6 class CUnifSp
11	9, 10	wcel 2144	. . . . 5 wff 𝑤 ∈ CUnifSp
12	7, 11	wa 401	. . . 4 wff (𝑢 ∈ ∪ ran UnifOn ∧ 𝑤 ∈ CUnifSp)
13		cuss 24577	. . . . . . 7 class UnifSt
14	9, 13	cfv 6538	. . . . . 6 class (UnifSt‘𝑤)
15	3	cuni 4866	. . . . . . 7 class ∪ 𝑢
16	15	cdm 5650	. . . . . 6 class dom ∪ 𝑢
17		crest 17596	. . . . . 6 class ↾t
18	14, 16, 17	co 7420	. . . . 5 class ((UnifSt‘𝑤) ↾t dom ∪ 𝑢)
19	18, 3	wceq 1569	. . . 4 wff ((UnifSt‘𝑤) ↾t dom ∪ 𝑢) = 𝑢
20		ctopn 17597	. . . . . . . 8 class TopOpen
21	9, 20	cfv 6538	. . . . . . 7 class (TopOpen‘𝑤)
22		ccl 23341	. . . . . . 7 class cls
23	21, 22	cfv 6538	. . . . . 6 class (cls‘(TopOpen‘𝑤))
24	16, 23	cfv 6538	. . . . 5 class ((cls‘(TopOpen‘𝑤))‘dom ∪ 𝑢)
25		cbs 17392	. . . . . 6 class Base
26	9, 25	cfv 6538	. . . . 5 class (Base‘𝑤)
27	24, 26	wceq 1569	. . . 4 wff ((cls‘(TopOpen‘𝑤))‘dom ∪ 𝑢) = (Base‘𝑤)
28	12, 19, 27	w3a 1103	. . 3 wff ((𝑢 ∈ ∪ ran UnifOn ∧ 𝑤 ∈ CUnifSp) ∧ ((UnifSt‘𝑤) ↾t dom ∪ 𝑢) = 𝑢 ∧ ((cls‘(TopOpen‘𝑤))‘dom ∪ 𝑢) = (Base‘𝑤))
29	28, 2, 8	copab 5166	. 2 class {⟨𝑢, 𝑤⟩ ∣ ((𝑢 ∈ ∪ ran UnifOn ∧ 𝑤 ∈ CUnifSp) ∧ ((UnifSt‘𝑤) ↾t dom ∪ 𝑢) = 𝑢 ∧ ((cls‘(TopOpen‘𝑤))‘dom ∪ 𝑢) = (Base‘𝑤))}
30	1, 29	wceq 1569	1 wff HCmp = {⟨𝑢, 𝑤⟩ ∣ ((𝑢 ∈ ∪ ran UnifOn ∧ 𝑤 ∈ CUnifSp) ∧ ((UnifSt‘𝑤) ↾t dom ∪ 𝑢) = 𝑢 ∧ ((cls‘(TopOpen‘𝑤))‘dom ∪ 𝑢) = (Base‘𝑤))}

This definition is used by: (None)