Definition df-cusp 23803

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 23802	. 2 class CUnifSp
2		vc	. . . . . . 7 setvar 𝑐
3	2	cv 1541	. . . . . 6 class 𝑐
4		vw	. . . . . . . . 9 setvar 𝑤
5	4	cv 1541	. . . . . . . 8 class 𝑤
6		cuss 23758	. . . . . . . 8 class UnifSt
7	5, 6	cfv 6544	. . . . . . 7 class (UnifSt‘𝑤)
8		ccfilu 23791	. . . . . . 7 class CauFilu
9	7, 8	cfv 6544	. . . . . 6 class (CauFilu‘(UnifSt‘𝑤))
10	3, 9	wcel 2107	. . . . 5 wff 𝑐 ∈ (CauFilu‘(UnifSt‘𝑤))
11		ctopn 17367	. . . . . . . 8 class TopOpen
12	5, 11	cfv 6544	. . . . . . 7 class (TopOpen‘𝑤)
13		cflim 23438	. . . . . . 7 class fLim
14	12, 3, 13	co 7409	. . . . . 6 class ((TopOpen‘𝑤) fLim 𝑐)
15		c0 4323	. . . . . 6 class ∅
16	14, 15	wne 2941	. . . . 5 wff ((TopOpen‘𝑤) fLim 𝑐) ≠ ∅
17	10, 16	wi 4	. . . 4 wff (𝑐 ∈ (CauFilu‘(UnifSt‘𝑤)) → ((TopOpen‘𝑤) fLim 𝑐) ≠ ∅)
18		cbs 17144	. . . . . 6 class Base
19	5, 18	cfv 6544	. . . . 5 class (Base‘𝑤)
20		cfil 23349	. . . . 5 class Fil
21	19, 20	cfv 6544	. . . 4 class (Fil‘(Base‘𝑤))
22	17, 2, 21	wral 3062	. . 3 wff ∀𝑐 ∈ (Fil‘(Base‘𝑤))(𝑐 ∈ (CauFilu‘(UnifSt‘𝑤)) → ((TopOpen‘𝑤) fLim 𝑐) ≠ ∅)
23		cusp 23759	. . 3 class UnifSp
24	22, 4, 23	crab 3433	. 2 class {𝑤 ∈ UnifSp ∣ ∀𝑐 ∈ (Fil‘(Base‘𝑤))(𝑐 ∈ (CauFilu‘(UnifSt‘𝑤)) → ((TopOpen‘𝑤) fLim 𝑐) ≠ ∅)}
25	1, 24	wceq 1542	1 wff CUnifSp = {𝑤 ∈ UnifSp ∣ ∀𝑐 ∈ (Fil‘(Base‘𝑤))(𝑐 ∈ (CauFilu‘(UnifSt‘𝑤)) → ((TopOpen‘𝑤) fLim 𝑐) ≠ ∅)}

This definition is referenced by:  iscusp  23804