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	⊢ ( 𝐴 ∈ On → suc 𝐴 ∈ ( TopOn ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		onsuctop	⊢ ( 𝐴 ∈ On → suc 𝐴 ∈ Top )
2		eloni	⊢ ( 𝐴 ∈ On → Ord 𝐴 )
3		ordunisuc	⊢ ( Ord 𝐴 → ∪ suc 𝐴 = 𝐴 )
4	3	eqcomd	⊢ ( Ord 𝐴 → 𝐴 = ∪ suc 𝐴 )
5	2 4	syl	⊢ ( 𝐴 ∈ On → 𝐴 = ∪ suc 𝐴 )
6		istopon	⊢ ( suc 𝐴 ∈ ( TopOn ‘ 𝐴 ) ↔ ( suc 𝐴 ∈ Top ∧ 𝐴 = ∪ suc 𝐴 ) )
7	1 5 6	sylanbrc	⊢ ( 𝐴 ∈ On → suc 𝐴 ∈ ( TopOn ‘ 𝐴 ) )