Definition 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 e. U. ran UnifOn /\ w e. CUnifSp ) /\ ( ( UnifSt ` w ) |`t dom U. u ) = u /\ ( ( cls ` ( TopOpen ` w ) ) ` dom U. u ) = ( Base ` w ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chcmp	|- HCmp
1		vu	|- u
2		vw	|- w
3	1	cv	|- u
4		cust	|- UnifOn
5	4	crn	|- ran UnifOn
6	5	cuni	|- U. ran UnifOn
7	3 6	wcel	|- u e. U. ran UnifOn
8	2	cv	|- w
9		ccusp	|- CUnifSp
10	8 9	wcel	|- w e. CUnifSp
11	7 10	wa	|- ( u e. U. ran UnifOn /\ w e. CUnifSp )
12		cuss	|- UnifSt
13	8 12	cfv	|- ( UnifSt ` w )
14		crest	|- |`t
15	3	cuni	|- U. u
16	15	cdm	|- dom U. u
17	13 16 14	co	|- ( ( UnifSt ` w ) |`t dom U. u )
18	17 3	wceq	|- ( ( UnifSt ` w ) |`t dom U. u ) = u
19		ccl	|- cls
20		ctopn	|- TopOpen
21	8 20	cfv	|- ( TopOpen ` w )
22	21 19	cfv	|- ( cls ` ( TopOpen ` w ) )
23	16 22	cfv	|- ( ( cls ` ( TopOpen ` w ) ) ` dom U. u )
24		cbs	|- Base
25	8 24	cfv	|- ( Base ` w )
26	23 25	wceq	|- ( ( cls ` ( TopOpen ` w ) ) ` dom U. u ) = ( Base ` w )
27	11 18 26	w3a	|- ( ( u e. U. ran UnifOn /\ w e. CUnifSp ) /\ ( ( UnifSt ` w ) |`t dom U. u ) = u /\ ( ( cls ` ( TopOpen ` w ) ) ` dom U. u ) = ( Base ` w ) )
28	27 1 2	copab	|- { <. 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 ) ) }
29	0 28	wceq	|- 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 ) ) }