Definition df-cusp 23358

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 23357	. 2 class CUnifSp
2		vc	. . . . . . 7 setvar 𝑐
3	2	cv 1538	. . . . . 6 class 𝑐
4		vw	. . . . . . . . 9 setvar 𝑤
5	4	cv 1538	. . . . . . . 8 class 𝑤
6		cuss 23313	. . . . . . . 8 class UnifSt
7	5, 6	cfv 6418	. . . . . . 7 class (UnifSt‘𝑤)
8		ccfilu 23346	. . . . . . 7 class CauFilu
9	7, 8	cfv 6418	. . . . . 6 class (CauFilu‘(UnifSt‘𝑤))
10	3, 9	wcel 2108	. . . . 5 wff 𝑐 ∈ (CauFilu‘(UnifSt‘𝑤))
11		ctopn 17049	. . . . . . . 8 class TopOpen
12	5, 11	cfv 6418	. . . . . . 7 class (TopOpen‘𝑤)
13		cflim 22993	. . . . . . 7 class fLim
14	12, 3, 13	co 7255	. . . . . 6 class ((TopOpen‘𝑤) fLim 𝑐)
15		c0 4253	. . . . . 6 class ∅
16	14, 15	wne 2942	. . . . 5 wff ((TopOpen‘𝑤) fLim 𝑐) ≠ ∅
17	10, 16	wi 4	. . . 4 wff (𝑐 ∈ (CauFilu‘(UnifSt‘𝑤)) → ((TopOpen‘𝑤) fLim 𝑐) ≠ ∅)
18		cbs 16840	. . . . . 6 class Base
19	5, 18	cfv 6418	. . . . 5 class (Base‘𝑤)
20		cfil 22904	. . . . 5 class Fil
21	19, 20	cfv 6418	. . . 4 class (Fil‘(Base‘𝑤))
22	17, 2, 21	wral 3063	. . 3 wff ∀𝑐 ∈ (Fil‘(Base‘𝑤))(𝑐 ∈ (CauFilu‘(UnifSt‘𝑤)) → ((TopOpen‘𝑤) fLim 𝑐) ≠ ∅)
23		cusp 23314	. . 3 class UnifSp
24	22, 4, 23	crab 3067	. 2 class {𝑤 ∈ UnifSp ∣ ∀𝑐 ∈ (Fil‘(Base‘𝑤))(𝑐 ∈ (CauFilu‘(UnifSt‘𝑤)) → ((TopOpen‘𝑤) fLim 𝑐) ≠ ∅)}
25	1, 24	wceq 1539	1 wff CUnifSp = {𝑤 ∈ UnifSp ∣ ∀𝑐 ∈ (Fil‘(Base‘𝑤))(𝑐 ∈ (CauFilu‘(UnifSt‘𝑤)) → ((TopOpen‘𝑤) fLim 𝑐) ≠ ∅)}

This definition is referenced by:  iscusp  23359