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	$$⊢\mathrm{On}\subseteq \mathrm{TopBases}$$

Proof

Step	Hyp	Ref	Expression
1		ontopbas	$$⊢x\in \mathrm{On}\to x\in \mathrm{TopBases}$$
2	1	ssriv	$$⊢\mathrm{On}\subseteq \mathrm{TopBases}$$