Theorem ontgsucval

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

	Ref	Expression
Assertion	ontgsucval	⊢ ( 𝐴 ∈ On → ( topGen ‘ suc 𝐴 ) = suc 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		suceloni	⊢ ( 𝐴 ∈ On → suc 𝐴 ∈ On )
2		ontgval	⊢ ( suc 𝐴 ∈ On → ( topGen ‘ suc 𝐴 ) = suc ∪ suc 𝐴 )
3	1 2	syl	⊢ ( 𝐴 ∈ On → ( topGen ‘ suc 𝐴 ) = suc ∪ suc 𝐴 )
4		eloni	⊢ ( 𝐴 ∈ On → Ord 𝐴 )
5		ordunisuc	⊢ ( Ord 𝐴 → ∪ suc 𝐴 = 𝐴 )
6	4 5	syl	⊢ ( 𝐴 ∈ On → ∪ suc 𝐴 = 𝐴 )
7		suceq	⊢ ( ∪ suc 𝐴 = 𝐴 → suc ∪ suc 𝐴 = suc 𝐴 )
8	6 7	syl	⊢ ( 𝐴 ∈ On → suc ∪ suc 𝐴 = suc 𝐴 )
9	3 8	eqtrd	⊢ ( 𝐴 ∈ On → ( topGen ‘ suc 𝐴 ) = suc 𝐴 )