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 ∈ On → suc ⁡ A ∈ Top

Proof

Step Hyp Ref Expression
1 ontgsucval ⊢ A ∈ On → topGen ⁡ suc ⁡ A = suc ⁡ A
2 suceloni ⊢ A ∈ On → suc ⁡ A ∈ On
3 ontopbas ⊢ suc ⁡ A ∈ On → suc ⁡ A ∈ TopBases
4 tgcl ⊢ suc ⁡ A ∈ TopBases → topGen ⁡ suc ⁡ A ∈ Top
5 2 3 4 3syl ⊢ A ∈ On → topGen ⁡ suc ⁡ A ∈ Top
6 1 5 eqeltrrd ⊢ A ∈ On → suc ⁡ A ∈ Top