This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ TopOpen Fn V

Proof

Step Hyp Ref Expression
1 ovex ⊢ TopSet ⁡ w ↾ 𝑡 Base w ∈ V
2 df-topn ⊢ TopOpen = w ∈ V ⟼ TopSet ⁡ w ↾ 𝑡 Base w
3 1 2 fnmpti ⊢ TopOpen Fn V