Theorem fntopon

Description: The class TopOn is a function with domain the universal class _V . Analogue for topologies of fnmre for Moore collections. (Contributed by BJ, 29-Apr-2021)

	Ref	Expression
Assertion	fntopon	⊢ TopOn Fn V

Proof

Step	Hyp	Ref	Expression
1		funtopon	⊢ Fun TopOn
2		dmtopon	⊢ dom TopOn = V
3		df-fn	⊢ ( TopOn Fn V ↔ ( Fun TopOn ∧ dom TopOn = V ) )
4	1 2 3	mpbir2an	⊢ TopOn Fn V