MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cusp Structured version   Visualization version   GIF version

Definition df-cusp 24023
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
StepHypRef Expression
1 ccusp 24022 . 2 class CUnifSp
2 vc . . . . . . 7 setvar ๐‘
32cv 1538 . . . . . 6 class ๐‘
4 vw . . . . . . . . 9 setvar ๐‘ค
54cv 1538 . . . . . . . 8 class ๐‘ค
6 cuss 23978 . . . . . . . 8 class UnifSt
75, 6cfv 6542 . . . . . . 7 class (UnifStโ€˜๐‘ค)
8 ccfilu 24011 . . . . . . 7 class CauFilu
97, 8cfv 6542 . . . . . 6 class (CauFiluโ€˜(UnifStโ€˜๐‘ค))
103, 9wcel 2104 . . . . 5 wff ๐‘ โˆˆ (CauFiluโ€˜(UnifStโ€˜๐‘ค))
11 ctopn 17371 . . . . . . . 8 class TopOpen
125, 11cfv 6542 . . . . . . 7 class (TopOpenโ€˜๐‘ค)
13 cflim 23658 . . . . . . 7 class fLim
1412, 3, 13co 7411 . . . . . 6 class ((TopOpenโ€˜๐‘ค) fLim ๐‘)
15 c0 4321 . . . . . 6 class โˆ…
1614, 15wne 2938 . . . . 5 wff ((TopOpenโ€˜๐‘ค) fLim ๐‘) โ‰  โˆ…
1710, 16wi 4 . . . 4 wff (๐‘ โˆˆ (CauFiluโ€˜(UnifStโ€˜๐‘ค)) โ†’ ((TopOpenโ€˜๐‘ค) fLim ๐‘) โ‰  โˆ…)
18 cbs 17148 . . . . . 6 class Base
195, 18cfv 6542 . . . . 5 class (Baseโ€˜๐‘ค)
20 cfil 23569 . . . . 5 class Fil
2119, 20cfv 6542 . . . 4 class (Filโ€˜(Baseโ€˜๐‘ค))
2217, 2, 21wral 3059 . . 3 wff โˆ€๐‘ โˆˆ (Filโ€˜(Baseโ€˜๐‘ค))(๐‘ โˆˆ (CauFiluโ€˜(UnifStโ€˜๐‘ค)) โ†’ ((TopOpenโ€˜๐‘ค) fLim ๐‘) โ‰  โˆ…)
23 cusp 23979 . . 3 class UnifSp
2422, 4, 23crab 3430 . 2 class {๐‘ค โˆˆ UnifSp โˆฃ โˆ€๐‘ โˆˆ (Filโ€˜(Baseโ€˜๐‘ค))(๐‘ โˆˆ (CauFiluโ€˜(UnifStโ€˜๐‘ค)) โ†’ ((TopOpenโ€˜๐‘ค) fLim ๐‘) โ‰  โˆ…)}
251, 24wceq 1539 1 wff CUnifSp = {๐‘ค โˆˆ UnifSp โˆฃ โˆ€๐‘ โˆˆ (Filโ€˜(Baseโ€˜๐‘ค))(๐‘ โˆˆ (CauFiluโ€˜(UnifStโ€˜๐‘ค)) โ†’ ((TopOpenโ€˜๐‘ค) fLim ๐‘) โ‰  โˆ…)}
Colors of variables: wff setvar class
This definition is referenced by:  iscusp  24024
  Copyright terms: Public domain W3C validator