Metamath Proof Explorer


Theorem topnid

Description: Value of the topology extractor function when the topology is defined over the same set as the base. (Contributed by Mario Carneiro, 13-Aug-2015)

Ref Expression
Hypotheses topnval.1 B=BaseW
topnval.2 J=TopSetW
Assertion topnid J𝒫BJ=TopOpenW

Proof

Step Hyp Ref Expression
1 topnval.1 B=BaseW
2 topnval.2 J=TopSetW
3 1 fvexi BV
4 restid2 BVJ𝒫BJ𝑡B=J
5 3 4 mpan J𝒫BJ𝑡B=J
6 1 2 topnval J𝑡B=TopOpenW
7 5 6 eqtr3di J𝒫BJ=TopOpenW