Definition df-hcmp 30003

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 unicity of such a completion. (Contributed by Thierry Arnoux, 5-Mar-2018.)

Assertion

Ref	Expression
df-hcmp	|- HCmp = { <. u , w >. | ( ( u e. U. ran UnifOn /\ w e. CUnifSp ) /\ ( (UnifSt ` w ) ↾t dom U. u ) = u /\ ( ( cls ` ( TopOpen ` w ) ) ` dom U. u ) = ( Base ` w ) ) }

Distinct variable group:   w, u

Detailed syntax breakdown of Definition df-hcmp

Step	Hyp	Ref	Expression
1		chcmp 30002	. 2 class HCmp
2		vu	. . . . . . 7 setvar u
3	2	cv 1482	. . . . . 6 class u
4		cust 22003	. . . . . . . 8 class UnifOn
5	4	crn 5115	. . . . . . 7 class ran UnifOn
6	5	cuni 4436	. . . . . 6 class U. ran UnifOn
7	3, 6	wcel 1990	. . . . 5 wff u e. U. ran UnifOn
8		vw	. . . . . . 7 setvar w
9	8	cv 1482	. . . . . 6 class w
10		ccusp 22101	. . . . . 6 class CUnifSp
11	9, 10	wcel 1990	. . . . 5 wff w e. CUnifSp
12	7, 11	wa 384	. . . 4 wff ( u e. U. ran UnifOn /\ w e. CUnifSp )
13		cuss 22057	. . . . . . 7 class UnifSt
14	9, 13	cfv 5888	. . . . . 6 class (UnifSt ` w )
15	3	cuni 4436	. . . . . . 7 class U. u
16	15	cdm 5114	. . . . . 6 class dom U. u
17		crest 16081	. . . . . 6 class ↾t
18	14, 16, 17	co 6650	. . . . 5 class ( (UnifSt ` w ) ↾t dom U. u )
19	18, 3	wceq 1483	. . . 4 wff ( (UnifSt ` w ) ↾t dom U. u ) = u
20		ctopn 16082	. . . . . . . 8 class TopOpen
21	9, 20	cfv 5888	. . . . . . 7 class ( TopOpen ` w )
22		ccl 20822	. . . . . . 7 class cls
23	21, 22	cfv 5888	. . . . . 6 class ( cls ` ( TopOpen ` w ) )
24	16, 23	cfv 5888	. . . . 5 class ( ( cls ` ( TopOpen ` w ) ) ` dom U. u )
25		cbs 15857	. . . . . 6 class Base
26	9, 25	cfv 5888	. . . . 5 class ( Base ` w )
27	24, 26	wceq 1483	. . . 4 wff ( ( cls ` ( TopOpen ` w ) ) ` dom U. u ) = ( Base ` w )
28	12, 19, 27	w3a 1037	. . 3 wff ( ( u e. U. ran UnifOn /\ w e. CUnifSp ) /\ ( (UnifSt ` w ) ↾t dom U. u ) = u /\ ( ( cls ` ( TopOpen ` w ) ) ` dom U. u ) = ( Base ` w ) )
29	28, 2, 8	copab 4712	. 2 class { <. u , w >. | ( ( u e. U. ran UnifOn /\ w e. CUnifSp ) /\ ( (UnifSt ` w ) ↾t dom U. u ) = u /\ ( ( cls ` ( TopOpen ` w ) ) ` dom U. u ) = ( Base ` w ) ) }
30	1, 29	wceq 1483	1 wff HCmp = { <. u , w >. | ( ( u e. U. ran UnifOn /\ w e. CUnifSp ) /\ ( (UnifSt ` w ) ↾t dom U. u ) = u /\ ( ( cls ` ( TopOpen ` w ) ) ` dom U. u ) = ( Base ` w ) ) }

This definition is referenced by: (None)