Metamath Proof Explorer


Theorem onsuctopon

Description: One of the topologies on an ordinal number is its successor. (Contributed by Chen-Pang He, 7-Nov-2015)

Ref Expression
Assertion onsuctopon A On suc A TopOn A

Proof

Step Hyp Ref Expression
1 onsuctop A On suc A Top
2 eloni A On Ord A
3 ordunisuc Ord A suc A = A
4 3 eqcomd Ord A A = suc A
5 2 4 syl A On A = suc A
6 istopon suc A TopOn A suc A Top A = suc A
7 1 5 6 sylanbrc A On suc A TopOn A