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

Proof

Step Hyp Ref Expression
1 ontgsucval 
 |-  ( A e. On -> ( topGen ` suc A ) = suc A )
2 suceloni 
 |-  ( A e. On -> suc A e. On )
3 ontopbas 
 |-  ( suc A e. On -> suc A e. TopBases )
4 tgcl 
 |-  ( suc A e. TopBases -> ( topGen ` suc A ) e. Top )
5 2 3 4 3syl 
 |-  ( A e. On -> ( topGen ` suc A ) e. Top )
6 1 5 eqeltrrd 
 |-  ( A e. On -> suc A e. Top )