MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-usp Structured version   Unicode version

Definition df-usp 19965
Description: Definition of a uniform space, i.e. a base set with an uniform structure and its induced topology. Derived from definition 3 of [BourbakiTop1] p. II.4. (Contributed by Thierry Arnoux, 17-Nov-2017.)
Assertion
Ref Expression
df-usp  |- UnifSp  =  {
f  |  ( (UnifSt `  f )  e.  (UnifOn `  ( Base `  f
) )  /\  ( TopOpen
`  f )  =  (unifTop `  (UnifSt `  f
) ) ) }

Detailed syntax breakdown of Definition df-usp
StepHypRef Expression
1 cusp 19962 . 2  class UnifSp
2 vf . . . . . . 7  setvar  f
32cv 1369 . . . . . 6  class  f
4 cuss 19961 . . . . . 6  class UnifSt
53, 4cfv 5527 . . . . 5  class  (UnifSt `  f )
6 cbs 14293 . . . . . . 7  class  Base
73, 6cfv 5527 . . . . . 6  class  ( Base `  f )
8 cust 19907 . . . . . 6  class UnifOn
97, 8cfv 5527 . . . . 5  class  (UnifOn `  ( Base `  f )
)
105, 9wcel 1758 . . . 4  wff  (UnifSt `  f )  e.  (UnifOn `  ( Base `  f
) )
11 ctopn 14480 . . . . . 6  class  TopOpen
123, 11cfv 5527 . . . . 5  class  ( TopOpen `  f )
13 cutop 19938 . . . . . 6  class unifTop
145, 13cfv 5527 . . . . 5  class  (unifTop `  (UnifSt `  f ) )
1512, 14wceq 1370 . . . 4  wff  ( TopOpen `  f )  =  (unifTop `  (UnifSt `  f )
)
1610, 15wa 369 . . 3  wff  ( (UnifSt `  f )  e.  (UnifOn `  ( Base `  f
) )  /\  ( TopOpen
`  f )  =  (unifTop `  (UnifSt `  f
) ) )
1716, 2cab 2439 . 2  class  { f  |  ( (UnifSt `  f )  e.  (UnifOn `  ( Base `  f
) )  /\  ( TopOpen
`  f )  =  (unifTop `  (UnifSt `  f
) ) ) }
181, 17wceq 1370 1  wff UnifSp  =  {
f  |  ( (UnifSt `  f )  e.  (UnifOn `  ( Base `  f
) )  /\  ( TopOpen
`  f )  =  (unifTop `  (UnifSt `  f
) ) ) }
Colors of variables: wff setvar class
This definition is referenced by:  isusp  19969
  Copyright terms: Public domain W3C validator