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 ) ) }