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 C_ TopBases

Proof

Step Hyp Ref Expression
1 ontopbas 
 |-  ( x e. On -> x e. TopBases )
2 1 ssriv 
 |-  On C_ TopBases