Metamath Proof Explorer


Syntax definition cpnrm

Description: Extend class notation with the class of all perfectly normal topologies.

Ref Expression
Assertion cpnrm class PNrm