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