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

Definition df-topsp 18482
Description: Define the class of all topological spaces (structures). (Contributed by Stefan O'Rear, 13-Aug-2015.)
Assertion
Ref Expression
df-topsp  |-  TopSp  =  {
f  |  ( TopOpen `  f )  e.  (TopOn `  ( Base `  f
) ) }

Detailed syntax breakdown of Definition df-topsp
StepHypRef Expression
1 ctps 18476 . 2  class  TopSp
2 vf . . . . . 6  setvar  f
32cv 1368 . . . . 5  class  f
4 ctopn 14352 . . . . 5  class  TopOpen
53, 4cfv 5413 . . . 4  class  ( TopOpen `  f )
6 cbs 14166 . . . . . 6  class  Base
73, 6cfv 5413 . . . . 5  class  ( Base `  f )
8 ctopon 18474 . . . . 5  class TopOn
97, 8cfv 5413 . . . 4  class  (TopOn `  ( Base `  f )
)
105, 9wcel 1756 . . 3  wff  ( TopOpen `  f )  e.  (TopOn `  ( Base `  f
) )
1110, 2cab 2424 . 2  class  { f  |  ( TopOpen `  f
)  e.  (TopOn `  ( Base `  f )
) }
121, 11wceq 1369 1  wff  TopSp  =  {
f  |  ( TopOpen `  f )  e.  (TopOn `  ( Base `  f
) ) }
Colors of variables: wff setvar class
This definition is referenced by:  istps  18516
  Copyright terms: Public domain W3C validator