Definition df-cusp

Description: Define the class of all complete uniform spaces. Definition 3 of BourbakiTop1 p. II.15. (Contributed by Thierry Arnoux, 1-Dec-2017)

	Ref	Expression
Assertion	df-cusp	⊢ CUnifSp = { 𝑤 ∈ UnifSp ∣ ∀ 𝑐 ∈ ( Fil ‘ ( Base ‘ 𝑤 ) ) ( 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑤 ) ) → ( ( TopOpen ‘ 𝑤 ) fLim 𝑐 ) ≠ ∅ ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccusp	⊢ CUnifSp
1		vw	⊢ 𝑤
2		cusp	⊢ UnifSp
3		vc	⊢ 𝑐
4		cfil	⊢ Fil
5		cbs	⊢ Base
6	1	cv	⊢ 𝑤
7	6 5	cfv	⊢ ( Base ‘ 𝑤 )
8	7 4	cfv	⊢ ( Fil ‘ ( Base ‘ 𝑤 ) )
9	3	cv	⊢ 𝑐
10		ccfilu	⊢ CauFilu
11		cuss	⊢ UnifSt
12	6 11	cfv	⊢ ( UnifSt ‘ 𝑤 )
13	12 10	cfv	⊢ ( CauFilu ‘ ( UnifSt ‘ 𝑤 ) )
14	9 13	wcel	⊢ 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑤 ) )
15		ctopn	⊢ TopOpen
16	6 15	cfv	⊢ ( TopOpen ‘ 𝑤 )
17		cflim	⊢ fLim
18	16 9 17	co	⊢ ( ( TopOpen ‘ 𝑤 ) fLim 𝑐 )
19		c0	⊢ ∅
20	18 19	wne	⊢ ( ( TopOpen ‘ 𝑤 ) fLim 𝑐 ) ≠ ∅
21	14 20	wi	⊢ ( 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑤 ) ) → ( ( TopOpen ‘ 𝑤 ) fLim 𝑐 ) ≠ ∅ )
22	21 3 8	wral	⊢ ∀ 𝑐 ∈ ( Fil ‘ ( Base ‘ 𝑤 ) ) ( 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑤 ) ) → ( ( TopOpen ‘ 𝑤 ) fLim 𝑐 ) ≠ ∅ )
23	22 1 2	crab	⊢ { 𝑤 ∈ UnifSp ∣ ∀ 𝑐 ∈ ( Fil ‘ ( Base ‘ 𝑤 ) ) ( 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑤 ) ) → ( ( TopOpen ‘ 𝑤 ) fLim 𝑐 ) ≠ ∅ ) }
24	0 23	wceq	⊢ CUnifSp = { 𝑤 ∈ UnifSp ∣ ∀ 𝑐 ∈ ( Fil ‘ ( Base ‘ 𝑤 ) ) ( 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑤 ) ) → ( ( TopOpen ‘ 𝑤 ) fLim 𝑐 ) ≠ ∅ ) }