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

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