This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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) \in TopOn ({Base}_{f})\}$

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