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

Proof

Step	Hyp	Ref	Expression
1		onsuctop	$$⊢A\in \mathrm{On}\to \mathrm{suc}A\in \mathrm{Top}$$
2		eloni	$$⊢A\in \mathrm{On}\to \mathrm{Ord}A$$
3		ordunisuc	$$⊢\mathrm{Ord}A\to \bigcup \mathrm{suc}A=A$$
4	3	eqcomd	$$⊢\mathrm{Ord}A\to A=\bigcup \mathrm{suc}A$$
5	2 4	syl	$$⊢A\in \mathrm{On}\to A=\bigcup \mathrm{suc}A$$
6		istopon	$$⊢\mathrm{suc}A\in \mathrm{TopOn}\left(A\right)\leftrightarrow \left(\mathrm{suc}A\in \mathrm{Top}\wedge A=\bigcup \mathrm{suc}A\right)$$
7	1 5 6	sylanbrc	$$⊢A\in \mathrm{On}\to \mathrm{suc}A\in \mathrm{TopOn}\left(A\right)$$