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	$$⊢\mathrm{TopSp}=\left\{f|\mathrm{TopOpen}\left(f\right)\in \mathrm{TopOn}\left({\mathrm{Base}}_f\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctps	$$class\mathrm{TopSp}$$
1		vf	$$setvarf$$
2		ctopn	$$class\mathrm{TopOpen}$$
3	1	cv	$$setvarf$$
4	3 2	cfv	$$class\mathrm{TopOpen}\left(f\right)$$
5		ctopon	$$class\mathrm{TopOn}$$
6		cbs	$$class\mathrm{Base}$$
7	3 6	cfv	$$class{\mathrm{Base}}_f$$
8	7 5	cfv	$$class\mathrm{TopOn}\left({\mathrm{Base}}_f\right)$$
9	4 8	wcel	$$wff\mathrm{TopOpen}\left(f\right)\in \mathrm{TopOn}\left({\mathrm{Base}}_f\right)$$
10	9 1	cab	$$class\left\{f|\mathrm{TopOpen}\left(f\right)\in \mathrm{TopOn}\left({\mathrm{Base}}_f\right)\right\}$$
11	0 10	wceq	$$wff\mathrm{TopSp}=\left\{f|\mathrm{TopOpen}\left(f\right)\in \mathrm{TopOn}\left({\mathrm{Base}}_f\right)\right\}$$