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 = Base W
topnval.2 J = TopSet W
Assertion topnval J 𝑡 B = TopOpen W

Proof

Step Hyp Ref Expression
1 topnval.1 B = Base W
2 topnval.2 J = TopSet W
3 fveq2 w = W TopSet w = TopSet W
4 3 2 syl6eqr w = W TopSet w = J
5 fveq2 w = W Base w = Base W
6 5 1 syl6eqr w = W Base w = B
7 4 6 oveq12d w = W TopSet w 𝑡 Base w = J 𝑡 B
8 df-topn TopOpen = w V TopSet w 𝑡 Base w
9 ovex J 𝑡 B V
10 7 8 9 fvmpt W V TopOpen W = J 𝑡 B
11 10 eqcomd W V J 𝑡 B = TopOpen W
12 0rest 𝑡 B =
13 fvprc ¬ W V TopSet W =
14 2 13 syl5eq ¬ W V J =
15 14 oveq1d ¬ W V J 𝑡 B = 𝑡 B
16 fvprc ¬ W V TopOpen W =
17 12 15 16 3eqtr4a ¬ W V J 𝑡 B = TopOpen W
18 11 17 pm2.61i J 𝑡 B = TopOpen W