Metamath Proof Explorer


Definition df-topsp

Description: Define the class of topological spaces (as extensible structures). (Contributed by Stefan O'Rear, 13-Aug-2015)

Ref Expression
Assertion df-topsp
|- TopSp = { f | ( TopOpen ` f ) e. ( TopOn ` ( Base ` f ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctps
 |-  TopSp
1 vf
 |-  f
2 ctopn
 |-  TopOpen
3 1 cv
 |-  f
4 3 2 cfv
 |-  ( TopOpen ` f )
5 ctopon
 |-  TopOn
6 cbs
 |-  Base
7 3 6 cfv
 |-  ( Base ` f )
8 7 5 cfv
 |-  ( TopOn ` ( Base ` f ) )
9 4 8 wcel
 |-  ( TopOpen ` f ) e. ( TopOn ` ( Base ` f ) )
10 9 1 cab
 |-  { f | ( TopOpen ` f ) e. ( TopOn ` ( Base ` f ) ) }
11 0 10 wceq
 |-  TopSp = { f | ( TopOpen ` f ) e. ( TopOn ` ( Base ` f ) ) }