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	$$⊢\mathrm{TopOn}Fn\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		funtopon	$$⊢\mathrm{Fun}\mathrm{TopOn}$$
2		dmtopon	$$⊢\mathrm{dom}\mathrm{TopOn}=\mathrm{V}$$
3		df-fn	$$⊢\mathrm{TopOn}Fn\mathrm{V}\leftrightarrow \left(\mathrm{Fun}\mathrm{TopOn}\wedge \mathrm{dom}\mathrm{TopOn}=\mathrm{V}\right)$$
4	1 2 3	mpbir2an	$$⊢\mathrm{TopOn}Fn\mathrm{V}$$