Definition df-topn

Description: Define the topology extractor function. This differs from df-tset when a structure has been restricted using df-ress ; in this case the TopSet component will still have a topology over the larger set, and this function fixes this by restricting the topology as well. (Contributed by Mario Carneiro, 13-Aug-2015)

	Ref	Expression
Assertion	df-topn	$$⊢\mathrm{TopOpen}=\left(w\in \mathrm{V}⟼\mathrm{TopSet}\left(w\right){\upharpoonright }_{𝑡}{\mathrm{Base}}_w\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctopn	$$class\mathrm{TopOpen}$$
1		vw	$$setvarw$$
2		cvv	$$class\mathrm{V}$$
3		cts	$$class\mathrm{TopSet}$$
4	1	cv	$$setvarw$$
5	4 3	cfv	$$class\mathrm{TopSet}\left(w\right)$$
6		crest	$$class{\upharpoonright }_{𝑡}$$
7		cbs	$$class\mathrm{Base}$$
8	4 7	cfv	$$class{\mathrm{Base}}_w$$
9	5 8 6	co	$$class\left(\mathrm{TopSet}\left(w\right){\upharpoonright }_{𝑡}{\mathrm{Base}}_w\right)$$
10	1 2 9	cmpt	$$class\left(w\in \mathrm{V}⟼\mathrm{TopSet}\left(w\right){\upharpoonright }_{𝑡}{\mathrm{Base}}_w\right)$$
11	0 10	wceq	$$wff\mathrm{TopOpen}=\left(w\in \mathrm{V}⟼\mathrm{TopSet}\left(w\right){\upharpoonright }_{𝑡}{\mathrm{Base}}_w\right)$$