Metamath Proof Explorer


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