Metamath Proof Explorer


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 ‘ 𝑤 ) ) )