Definition df-cusp 22102

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

Assertion

Ref	Expression
df-cusp	|- CUnifSp = { w e. UnifSp | A. c e. ( Fil ` ( Base ` w ) ) ( c e. (CauFilu ` (UnifSt ` w ) ) -> ( ( TopOpen ` w ) fLim c ) =/= (/) ) }

Distinct variable group:   w, c

Detailed syntax breakdown of Definition df-cusp

Step	Hyp	Ref	Expression
1		ccusp 22101	. 2 class CUnifSp
2		vc	. . . . . . 7 setvar c
3	2	cv 1482	. . . . . 6 class c
4		vw	. . . . . . . . 9 setvar w
5	4	cv 1482	. . . . . . . 8 class w
6		cuss 22057	. . . . . . . 8 class UnifSt
7	5, 6	cfv 5888	. . . . . . 7 class (UnifSt ` w )
8		ccfilu 22090	. . . . . . 7 class CauFilu
9	7, 8	cfv 5888	. . . . . 6 class (CauFilu ` (UnifSt ` w ) )
10	3, 9	wcel 1990	. . . . 5 wff c e. (CauFilu ` (UnifSt ` w ) )
11		ctopn 16082	. . . . . . . 8 class TopOpen
12	5, 11	cfv 5888	. . . . . . 7 class ( TopOpen ` w )
13		cflim 21738	. . . . . . 7 class fLim
14	12, 3, 13	co 6650	. . . . . 6 class ( ( TopOpen ` w ) fLim c )
15		c0 3915	. . . . . 6 class (/)
16	14, 15	wne 2794	. . . . 5 wff ( ( TopOpen ` w ) fLim c ) =/= (/)
17	10, 16	wi 4	. . . 4 wff ( c e. (CauFilu ` (UnifSt ` w ) ) -> ( ( TopOpen ` w ) fLim c ) =/= (/) )
18		cbs 15857	. . . . . 6 class Base
19	5, 18	cfv 5888	. . . . 5 class ( Base ` w )
20		cfil 21649	. . . . 5 class Fil
21	19, 20	cfv 5888	. . . 4 class ( Fil ` ( Base ` w ) )
22	17, 2, 21	wral 2912	. . 3 wff A. c e. ( Fil ` ( Base ` w ) ) ( c e. (CauFilu ` (UnifSt ` w ) ) -> ( ( TopOpen ` w ) fLim c ) =/= (/) )
23		cusp 22058	. . 3 class UnifSp
24	22, 4, 23	crab 2916	. 2 class { w e. UnifSp | A. c e. ( Fil ` ( Base ` w ) ) ( c e. (CauFilu ` (UnifSt ` w ) ) -> ( ( TopOpen ` w ) fLim c ) =/= (/) ) }
25	1, 24	wceq 1483	1 wff CUnifSp = { w e. UnifSp | A. c e. ( Fil ` ( Base ` w ) ) ( c e. (CauFilu ` (UnifSt ` w ) ) -> ( ( TopOpen ` w ) fLim c ) =/= (/) ) }

This definition is referenced by:  iscusp  22103