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 ) |`t ( Base ` w ) ) e. _V
2 df-topn 
 |-  TopOpen = ( w e. _V |-> ( ( TopSet ` w ) |`t ( Base ` w ) ) )
3 1 2 fnmpti 
 |-  TopOpen Fn _V