Definition df-cusp 21912

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 = {𝑤 ∈ UnifSp ∣ ∀𝑐 ∈ (Fil‘(Base‘𝑤))(𝑐 ∈ (CauFilu‘(UnifSt‘𝑤)) → ((TopOpen‘𝑤) fLim 𝑐) ≠ ∅)}

Distinct variable group:   𝑤,𝑐

Detailed syntax breakdown of Definition df-cusp

Step	Hyp	Ref	Expression
1		ccusp 21911	. 2 class CUnifSp
2		vc	. . . . . . 7 setvar 𝑐
3	2	cv 1474	. . . . . 6 class 𝑐
4		vw	. . . . . . . . 9 setvar 𝑤
5	4	cv 1474	. . . . . . . 8 class 𝑤
6		cuss 21867	. . . . . . . 8 class UnifSt
7	5, 6	cfv 5804	. . . . . . 7 class (UnifSt‘𝑤)
8		ccfilu 21900	. . . . . . 7 class CauFilu
9	7, 8	cfv 5804	. . . . . 6 class (CauFilu‘(UnifSt‘𝑤))
10	3, 9	wcel 1977	. . . . 5 wff 𝑐 ∈ (CauFilu‘(UnifSt‘𝑤))
11		ctopn 15905	. . . . . . . 8 class TopOpen
12	5, 11	cfv 5804	. . . . . . 7 class (TopOpen‘𝑤)
13		cflim 21548	. . . . . . 7 class fLim
14	12, 3, 13	co 6549	. . . . . 6 class ((TopOpen‘𝑤) fLim 𝑐)
15		c0 3874	. . . . . 6 class ∅
16	14, 15	wne 2780	. . . . 5 wff ((TopOpen‘𝑤) fLim 𝑐) ≠ ∅
17	10, 16	wi 4	. . . 4 wff (𝑐 ∈ (CauFilu‘(UnifSt‘𝑤)) → ((TopOpen‘𝑤) fLim 𝑐) ≠ ∅)
18		cbs 15695	. . . . . 6 class Base
19	5, 18	cfv 5804	. . . . 5 class (Base‘𝑤)
20		cfil 21459	. . . . 5 class Fil
21	19, 20	cfv 5804	. . . 4 class (Fil‘(Base‘𝑤))
22	17, 2, 21	wral 2896	. . 3 wff ∀𝑐 ∈ (Fil‘(Base‘𝑤))(𝑐 ∈ (CauFilu‘(UnifSt‘𝑤)) → ((TopOpen‘𝑤) fLim 𝑐) ≠ ∅)
23		cusp 21868	. . 3 class UnifSp
24	22, 4, 23	crab 2900	. 2 class {𝑤 ∈ UnifSp ∣ ∀𝑐 ∈ (Fil‘(Base‘𝑤))(𝑐 ∈ (CauFilu‘(UnifSt‘𝑤)) → ((TopOpen‘𝑤) fLim 𝑐) ≠ ∅)}
25	1, 24	wceq 1475	1 wff CUnifSp = {𝑤 ∈ UnifSp ∣ ∀𝑐 ∈ (Fil‘(Base‘𝑤))(𝑐 ∈ (CauFilu‘(UnifSt‘𝑤)) → ((TopOpen‘𝑤) fLim 𝑐) ≠ ∅)}

This definition is referenced by:  iscusp  21913