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	$⊢ HCmp = \{⟨u, w⟩ \| ((u \in ⋃ ran UnifOn \land w \in CUnifSp) \land UnifSt (w) ↾_{𝑡} dom ⋃ u = u \land cls (TopOpen (w)) (dom ⋃ u) = {Base}_{w})\}$

Detailed syntax breakdown

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

Metamath Proof Explorer

Definition df-hcmp

Detailed syntax breakdown