# Metamath Proof Explorer

## Theorem topnval

Description: Value of the topology extractor function. (Contributed by Mario Carneiro, 13-Aug-2015)

Ref Expression
Hypotheses topnval.1 ${⊢}{B}={\mathrm{Base}}_{{W}}$
topnval.2 ${⊢}{J}=\mathrm{TopSet}\left({W}\right)$
Assertion topnval ${⊢}{J}{↾}_{𝑡}{B}=\mathrm{TopOpen}\left({W}\right)$

### Proof

Step Hyp Ref Expression
1 topnval.1 ${⊢}{B}={\mathrm{Base}}_{{W}}$
2 topnval.2 ${⊢}{J}=\mathrm{TopSet}\left({W}\right)$
3 fveq2 ${⊢}{w}={W}\to \mathrm{TopSet}\left({w}\right)=\mathrm{TopSet}\left({W}\right)$
4 3 2 syl6eqr ${⊢}{w}={W}\to \mathrm{TopSet}\left({w}\right)={J}$
5 fveq2 ${⊢}{w}={W}\to {\mathrm{Base}}_{{w}}={\mathrm{Base}}_{{W}}$
6 5 1 syl6eqr ${⊢}{w}={W}\to {\mathrm{Base}}_{{w}}={B}$
7 4 6 oveq12d ${⊢}{w}={W}\to \mathrm{TopSet}\left({w}\right){↾}_{𝑡}{\mathrm{Base}}_{{w}}={J}{↾}_{𝑡}{B}$
8 df-topn ${⊢}\mathrm{TopOpen}=\left({w}\in \mathrm{V}⟼\mathrm{TopSet}\left({w}\right){↾}_{𝑡}{\mathrm{Base}}_{{w}}\right)$
9 ovex ${⊢}{J}{↾}_{𝑡}{B}\in \mathrm{V}$
10 7 8 9 fvmpt ${⊢}{W}\in \mathrm{V}\to \mathrm{TopOpen}\left({W}\right)={J}{↾}_{𝑡}{B}$
11 10 eqcomd ${⊢}{W}\in \mathrm{V}\to {J}{↾}_{𝑡}{B}=\mathrm{TopOpen}\left({W}\right)$
12 0rest ${⊢}\varnothing {↾}_{𝑡}{B}=\varnothing$
13 fvprc ${⊢}¬{W}\in \mathrm{V}\to \mathrm{TopSet}\left({W}\right)=\varnothing$
14 2 13 syl5eq ${⊢}¬{W}\in \mathrm{V}\to {J}=\varnothing$
15 14 oveq1d ${⊢}¬{W}\in \mathrm{V}\to {J}{↾}_{𝑡}{B}=\varnothing {↾}_{𝑡}{B}$
16 fvprc ${⊢}¬{W}\in \mathrm{V}\to \mathrm{TopOpen}\left({W}\right)=\varnothing$
17 12 15 16 3eqtr4a ${⊢}¬{W}\in \mathrm{V}\to {J}{↾}_{𝑡}{B}=\mathrm{TopOpen}\left({W}\right)$
18 11 17 pm2.61i ${⊢}{J}{↾}_{𝑡}{B}=\mathrm{TopOpen}\left({W}\right)$