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	⊢ TopOpen = ( 𝑤 ∈ V ↦ ( ( TopSet ‘ 𝑤 ) ↾t ( Base ‘ 𝑤 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctopn	⊢ TopOpen
1		vw	⊢ 𝑤
2		cvv	⊢ V
3		cts	⊢ TopSet
4	1	cv	⊢ 𝑤
5	4 3	cfv	⊢ ( TopSet ‘ 𝑤 )
6		crest	⊢ ↾t
7		cbs	⊢ Base
8	4 7	cfv	⊢ ( Base ‘ 𝑤 )
9	5 8 6	co	⊢ ( ( TopSet ‘ 𝑤 ) ↾t ( Base ‘ 𝑤 ) )
10	1 2 9	cmpt	⊢ ( 𝑤 ∈ V ↦ ( ( TopSet ‘ 𝑤 ) ↾t ( Base ‘ 𝑤 ) ) )
11	0 10	wceq	⊢ TopOpen = ( 𝑤 ∈ V ↦ ( ( TopSet ‘ 𝑤 ) ↾t ( Base ‘ 𝑤 ) ) )