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 = { ⟨ 𝑢 , 𝑤 ⟩ ∣ ( ( 𝑢 ∈ ∪ ran UnifOn ∧ 𝑤 ∈ CUnifSp ) ∧ ( ( UnifSt ‘ 𝑤 ) ↾t dom ∪ 𝑢 ) = 𝑢 ∧ ( ( cls ‘ ( TopOpen ‘ 𝑤 ) ) ‘ dom ∪ 𝑢 ) = ( Base ‘ 𝑤 ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chcmp	⊢ HCmp
1		vu	⊢ 𝑢
2		vw	⊢ 𝑤
3	1	cv	⊢ 𝑢
4		cust	⊢ UnifOn
5	4	crn	⊢ ran UnifOn
6	5	cuni	⊢ ∪ ran UnifOn
7	3 6	wcel	⊢ 𝑢 ∈ ∪ ran UnifOn
8	2	cv	⊢ 𝑤
9		ccusp	⊢ CUnifSp
10	8 9	wcel	⊢ 𝑤 ∈ CUnifSp
11	7 10	wa	⊢ ( 𝑢 ∈ ∪ ran UnifOn ∧ 𝑤 ∈ CUnifSp )
12		cuss	⊢ UnifSt
13	8 12	cfv	⊢ ( UnifSt ‘ 𝑤 )
14		crest	⊢ ↾t
15	3	cuni	⊢ ∪ 𝑢
16	15	cdm	⊢ dom ∪ 𝑢
17	13 16 14	co	⊢ ( ( UnifSt ‘ 𝑤 ) ↾t dom ∪ 𝑢 )
18	17 3	wceq	⊢ ( ( UnifSt ‘ 𝑤 ) ↾t dom ∪ 𝑢 ) = 𝑢
19		ccl	⊢ cls
20		ctopn	⊢ TopOpen
21	8 20	cfv	⊢ ( TopOpen ‘ 𝑤 )
22	21 19	cfv	⊢ ( cls ‘ ( TopOpen ‘ 𝑤 ) )
23	16 22	cfv	⊢ ( ( cls ‘ ( TopOpen ‘ 𝑤 ) ) ‘ dom ∪ 𝑢 )
24		cbs	⊢ Base
25	8 24	cfv	⊢ ( Base ‘ 𝑤 )
26	23 25	wceq	⊢ ( ( cls ‘ ( TopOpen ‘ 𝑤 ) ) ‘ dom ∪ 𝑢 ) = ( Base ‘ 𝑤 )
27	11 18 26	w3a	⊢ ( ( 𝑢 ∈ ∪ ran UnifOn ∧ 𝑤 ∈ CUnifSp ) ∧ ( ( UnifSt ‘ 𝑤 ) ↾t dom ∪ 𝑢 ) = 𝑢 ∧ ( ( cls ‘ ( TopOpen ‘ 𝑤 ) ) ‘ dom ∪ 𝑢 ) = ( Base ‘ 𝑤 ) )
28	27 1 2	copab	⊢ { ⟨ 𝑢 , 𝑤 ⟩ ∣ ( ( 𝑢 ∈ ∪ ran UnifOn ∧ 𝑤 ∈ CUnifSp ) ∧ ( ( UnifSt ‘ 𝑤 ) ↾t dom ∪ 𝑢 ) = 𝑢 ∧ ( ( cls ‘ ( TopOpen ‘ 𝑤 ) ) ‘ dom ∪ 𝑢 ) = ( Base ‘ 𝑤 ) ) }
29	0 28	wceq	⊢ HCmp = { ⟨ 𝑢 , 𝑤 ⟩ ∣ ( ( 𝑢 ∈ ∪ ran UnifOn ∧ 𝑤 ∈ CUnifSp ) ∧ ( ( UnifSt ‘ 𝑤 ) ↾t dom ∪ 𝑢 ) = 𝑢 ∧ ( ( cls ‘ ( TopOpen ‘ 𝑤 ) ) ‘ dom ∪ 𝑢 ) = ( Base ‘ 𝑤 ) ) }