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{\upharpoonright }_{𝑡}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	eqtr4di	$$⊢w=W\to \mathrm{TopSet}\left(w\right)=J$$
5		fveq2	$$⊢w=W\to {\mathrm{Base}}_w={\mathrm{Base}}_W$$
6	5 1	eqtr4di	$$⊢w=W\to {\mathrm{Base}}_w=B$$
7	4 6	oveq12d	$$⊢w=W\to \mathrm{TopSet}\left(w\right){\upharpoonright }_{𝑡}{\mathrm{Base}}_w=J{\upharpoonright }_{𝑡}B$$
8		df-topn	$$⊢\mathrm{TopOpen}=\left(w\in \mathrm{V}⟼\mathrm{TopSet}\left(w\right){\upharpoonright }_{𝑡}{\mathrm{Base}}_w\right)$$
9		ovex	$$⊢J{\upharpoonright }_{𝑡}B\in \mathrm{V}$$
10	7 8 9	fvmpt	$$⊢W\in \mathrm{V}\to \mathrm{TopOpen}\left(W\right)=J{\upharpoonright }_{𝑡}B$$
11	10	eqcomd	$$⊢W\in \mathrm{V}\to J{\upharpoonright }_{𝑡}B=\mathrm{TopOpen}\left(W\right)$$
12		0rest	$$⊢\varnothing {\upharpoonright }_{𝑡}B=\varnothing$$
13		fvprc	$$⊢\neg W\in \mathrm{V}\to \mathrm{TopSet}\left(W\right)=\varnothing$$
14	2 13	syl5eq	$$⊢\neg W\in \mathrm{V}\to J=\varnothing$$
15	14	oveq1d	$$⊢\neg W\in \mathrm{V}\to J{\upharpoonright }_{𝑡}B=\varnothing {\upharpoonright }_{𝑡}B$$
16		fvprc	$$⊢\neg W\in \mathrm{V}\to \mathrm{TopOpen}\left(W\right)=\varnothing$$
17	12 15 16	3eqtr4a	$$⊢\neg W\in \mathrm{V}\to J{\upharpoonright }_{𝑡}B=\mathrm{TopOpen}\left(W\right)$$
18	11 17	pm2.61i	$$⊢J{\upharpoonright }_{𝑡}B=\mathrm{TopOpen}\left(W\right)$$