Metamath Proof Explorer


Theorem onsuctop

Description: A successor ordinal number is a topology. (Contributed by Chen-Pang He, 11-Oct-2015)

Ref Expression
Assertion onsuctop AOnsucATop

Proof

Step Hyp Ref Expression
1 ontgsucval AOntopGensucA=sucA
2 suceloni AOnsucAOn
3 ontopbas sucAOnsucATopBases
4 tgcl sucATopBasestopGensucATop
5 2 3 4 3syl AOntopGensucATop
6 1 5 eqeltrrd AOnsucATop