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	|- ( A e. On -> ( topGen ` suc A ) = suc A )

Proof

Step	Hyp	Ref	Expression
1		onsuc	|- ( A e. On -> suc A e. On )
2		ontgval	|- ( suc A e. On -> ( topGen ` suc A ) = suc U. suc A )
3	1 2	syl	|- ( A e. On -> ( topGen ` suc A ) = suc U. suc A )
4		eloni	|- ( A e. On -> Ord A )
5		ordunisuc	|- ( Ord A -> U. suc A = A )
6	4 5	syl	|- ( A e. On -> U. suc A = A )
7		suceq	|- ( U. suc A = A -> suc U. suc A = suc A )
8	6 7	syl	|- ( A e. On -> suc U. suc A = suc A )
9	3 8	eqtrd	|- ( A e. On -> ( topGen ` suc A ) = suc A )