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 ‘ 𝑤 ) ↾t ( Base ‘ 𝑤 ) ) ∈ V
2		df-topn	⊢ TopOpen = ( 𝑤 ∈ V ↦ ( ( TopSet ‘ 𝑤 ) ↾t ( Base ‘ 𝑤 ) ) )
3	1 2	fnmpti	⊢ TopOpen Fn V