Metamath Proof Explorer


Theorem onsstopbas

Description: The class of ordinal numbers is a subclass of the class of topological bases. (Contributed by Chen-Pang He, 8-Oct-2015)

Ref Expression
Assertion onsstopbas On TopBases

Proof

Step Hyp Ref Expression
1 ontopbas x On x TopBases
2 1 ssriv On TopBases