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 = \{w \in UnifSp \| \forall c \in Fil ({Base}_{w}) (c \in CauFilU (UnifSt (w)) \to TopOpen (w) fLim c \neq \emptyset)\}$

Step	Hyp	Ref	Expression
0		ccusp	$class CUnifSp$
1		vw	$setvar w$
2		cusp	$class UnifSp$
3		vc	$setvar c$
4		cfil	$class Fil$
5		cbs	$class Base$
6	1	cv	$setvar w$
7	6 5	cfv	$class {Base}_{w}$
8	7 4	cfv	$class Fil ({Base}_{w})$
9	3	cv	$setvar c$
10		ccfilu	$class CauFilU$
11		cuss	$class UnifSt$
12	6 11	cfv	$class UnifSt (w)$
13	12 10	cfv	$class CauFilU (UnifSt (w))$
14	9 13	wcel	$wff c \in CauFilU (UnifSt (w))$
15		ctopn	$class TopOpen$
16	6 15	cfv	$class TopOpen (w)$
17		cflim	$class fLim$
18	16 9 17	co	$class (TopOpen (w) fLim c)$
19		c0	$class \emptyset$
20	18 19	wne	$wff TopOpen (w) fLim c \neq \emptyset$
21	14 20	wi	$wff (c \in CauFilU (UnifSt (w)) \to TopOpen (w) fLim c \neq \emptyset)$
22	21 3 8	wral	$wff \forall c \in Fil ({Base}_{w}) (c \in CauFilU (UnifSt (w)) \to TopOpen (w) fLim c \neq \emptyset)$
23	22 1 2	crab	$class \{w \in UnifSp \| \forall c \in Fil ({Base}_{w}) (c \in CauFilU (UnifSt (w)) \to TopOpen (w) fLim c \neq \emptyset)\}$
24	0 23	wceq	$wff CUnifSp = \{w \in UnifSp \| \forall c \in Fil ({Base}_{w}) (c \in CauFilU (UnifSt (w)) \to TopOpen (w) fLim c \neq \emptyset)\}$

Metamath Proof Explorer