Metamath Proof Explorer


Theorem funtopon

Description: The class TopOn is a function. (Contributed by BJ, 29-Apr-2021)

Ref Expression
Assertion funtopon FunTopOn

Proof

Step Hyp Ref Expression
1 df-topon TopOn=yVxTop|y=x
2 1 funmpt2 FunTopOn