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 e. On -> suc A e. ( TopOn ` A ) )

Proof

Step Hyp Ref Expression
1 onsuctop 
 |-  ( A e. On -> suc A e. Top )
2 eloni 
 |-  ( A e. On -> Ord A )
3 ordunisuc 
 |-  ( Ord A -> U. suc A = A )
4 3 eqcomd 
 |-  ( Ord A -> A = U. suc A )
5 2 4 syl 
 |-  ( A e. On -> A = U. suc A )
6 istopon 
 |-  ( suc A e. ( TopOn ` A ) <-> ( suc A e. Top /\ A = U. suc A ) )
7 1 5 6 sylanbrc 
 |-  ( A e. On -> suc A e. ( TopOn ` A ) )