Definition df-cusp 24307

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 24306	. 2 class CUnifSp
2		vc	. . . . . . 7 setvar 𝑐
3	2	cv 1539	. . . . . 6 class 𝑐
4		vw	. . . . . . . . 9 setvar 𝑤
5	4	cv 1539	. . . . . . . 8 class 𝑤
6		cuss 24262	. . . . . . . 8 class UnifSt
7	5, 6	cfv 6561	. . . . . . 7 class (UnifSt‘𝑤)
8		ccfilu 24295	. . . . . . 7 class CauFilu
9	7, 8	cfv 6561	. . . . . 6 class (CauFilu‘(UnifSt‘𝑤))
10	3, 9	wcel 2108	. . . . 5 wff 𝑐 ∈ (CauFilu‘(UnifSt‘𝑤))
11		ctopn 17466	. . . . . . . 8 class TopOpen
12	5, 11	cfv 6561	. . . . . . 7 class (TopOpen‘𝑤)
13		cflim 23942	. . . . . . 7 class fLim
14	12, 3, 13	co 7431	. . . . . 6 class ((TopOpen‘𝑤) fLim 𝑐)
15		c0 4333	. . . . . 6 class ∅
16	14, 15	wne 2940	. . . . 5 wff ((TopOpen‘𝑤) fLim 𝑐) ≠ ∅
17	10, 16	wi 4	. . . 4 wff (𝑐 ∈ (CauFilu‘(UnifSt‘𝑤)) → ((TopOpen‘𝑤) fLim 𝑐) ≠ ∅)
18		cbs 17247	. . . . . 6 class Base
19	5, 18	cfv 6561	. . . . 5 class (Base‘𝑤)
20		cfil 23853	. . . . 5 class Fil
21	19, 20	cfv 6561	. . . 4 class (Fil‘(Base‘𝑤))
22	17, 2, 21	wral 3061	. . 3 wff ∀𝑐 ∈ (Fil‘(Base‘𝑤))(𝑐 ∈ (CauFilu‘(UnifSt‘𝑤)) → ((TopOpen‘𝑤) fLim 𝑐) ≠ ∅)
23		cusp 24263	. . 3 class UnifSp
24	22, 4, 23	crab 3436	. 2 class {𝑤 ∈ UnifSp ∣ ∀𝑐 ∈ (Fil‘(Base‘𝑤))(𝑐 ∈ (CauFilu‘(UnifSt‘𝑤)) → ((TopOpen‘𝑤) fLim 𝑐) ≠ ∅)}
25	1, 24	wceq 1540	1 wff CUnifSp = {𝑤 ∈ UnifSp ∣ ∀𝑐 ∈ (Fil‘(Base‘𝑤))(𝑐 ∈ (CauFilu‘(UnifSt‘𝑤)) → ((TopOpen‘𝑤) fLim 𝑐) ≠ ∅)}

This definition is referenced by:  iscusp  24308