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	⊢ ( 𝑥 ∈ On → 𝑥 ∈ TopBases )
2	1	ssriv	⊢ On ⊆ TopBases