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 e. _V |-> ( ( TopSet ` w ) |`t ( Base ` w ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | ctopn | |- TopOpen |
|
| 1 | vw | |- w |
|
| 2 | cvv | |- _V |
|
| 3 | cts | |- TopSet |
|
| 4 | 1 | cv | |- w |
| 5 | 4 3 | cfv | |- ( TopSet ` w ) |
| 6 | crest | |- |`t |
|
| 7 | cbs | |- Base |
|
| 8 | 4 7 | cfv | |- ( Base ` w ) |
| 9 | 5 8 6 | co | |- ( ( TopSet ` w ) |`t ( Base ` w ) ) |
| 10 | 1 2 9 | cmpt | |- ( w e. _V |-> ( ( TopSet ` w ) |`t ( Base ` w ) ) ) |
| 11 | 0 10 | wceq | |- TopOpen = ( w e. _V |-> ( ( TopSet ` w ) |`t ( Base ` w ) ) ) |