Metamath Proof Explorer


Theorem topnfn

Description: The topology extractor function is a function on the universe. (Contributed by Mario Carneiro, 13-Aug-2015)

Ref Expression
Assertion topnfn TopOpenFnV

Proof

Step Hyp Ref Expression
1 ovex TopSetw𝑡BasewV
2 df-topn TopOpen=wVTopSetw𝑡Basew
3 1 2 fnmpti TopOpenFnV