Theorem onsuctop

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

	Ref	Expression
Assertion	onsuctop	⊢ ( 𝐴 ∈ On → suc 𝐴 ∈ Top )

Proof

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