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\in \mathrm{On}\to \mathrm{topGen}\left(\mathrm{suc}A\right)=\mathrm{suc}A$$

Proof

Step	Hyp	Ref	Expression
1		onsuc	$$⊢A\in \mathrm{On}\to \mathrm{suc}A\in \mathrm{On}$$
2		ontgval	$$⊢\mathrm{suc}A\in \mathrm{On}\to \mathrm{topGen}\left(\mathrm{suc}A\right)=\mathrm{suc}\bigcup \mathrm{suc}A$$
3	1 2	syl	$$⊢A\in \mathrm{On}\to \mathrm{topGen}\left(\mathrm{suc}A\right)=\mathrm{suc}\bigcup \mathrm{suc}A$$
4		eloni	$$⊢A\in \mathrm{On}\to \mathrm{Ord}A$$
5		ordunisuc	$$⊢\mathrm{Ord}A\to \bigcup \mathrm{suc}A=A$$
6	4 5	syl	$$⊢A\in \mathrm{On}\to \bigcup \mathrm{suc}A=A$$
7		suceq	$$⊢\bigcup \mathrm{suc}A=A\to \mathrm{suc}\bigcup \mathrm{suc}A=\mathrm{suc}A$$
8	6 7	syl	$$⊢A\in \mathrm{On}\to \mathrm{suc}\bigcup \mathrm{suc}A=\mathrm{suc}A$$
9	3 8	eqtrd	$$⊢A\in \mathrm{On}\to \mathrm{topGen}\left(\mathrm{suc}A\right)=\mathrm{suc}A$$