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 = w ∈ V ⟼ TopSet ⁡ w ↾ 𝑡 Base w

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctopn class TopOpen
1 vw setvar w
2 cvv class V
3 cts class TopSet
4 1 cv setvar w
5 4 3 cfv class TopSet ⁡ w
6 crest class ↾ 𝑡
7 cbs class Base
8 4 7 cfv class Base w
9 5 8 6 co class TopSet ⁡ w ↾ 𝑡 Base w
10 1 2 9 cmpt class w ∈ V ⟼ TopSet ⁡ w ↾ 𝑡 Base w
11 0 10 wceq wff TopOpen = w ∈ V ⟼ TopSet ⁡ w ↾ 𝑡 Base w