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

Definition df-topsp 20785
Description: Define the class of topological spaces (as extensible structures). (Contributed by Stefan O'Rear, 13-Aug-2015.)
Assertion
Ref Expression
df-topsp TopSp = {𝑓 ∣ (TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓))}

Detailed syntax breakdown of Definition df-topsp
StepHypRef Expression
1 ctps 20784 . 2 class TopSp
2 vf . . . . . 6 setvar 𝑓
32cv 1522 . . . . 5 class 𝑓
4 ctopn 16129 . . . . 5 class TopOpen
53, 4cfv 5926 . . . 4 class (TopOpen‘𝑓)
6 cbs 15904 . . . . . 6 class Base
73, 6cfv 5926 . . . . 5 class (Base‘𝑓)
8 ctopon 20763 . . . . 5 class TopOn
97, 8cfv 5926 . . . 4 class (TopOn‘(Base‘𝑓))
105, 9wcel 2030 . . 3 wff (TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓))
1110, 2cab 2637 . 2 class {𝑓 ∣ (TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓))}
121, 11wceq 1523 1 wff TopSp = {𝑓 ∣ (TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓))}
Colors of variables: wff setvar class
This definition is referenced by:  istps  20786
  Copyright terms: Public domain W3C validator