This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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