Theorem ordtop

Description: An ordinal is a topology iff it is not its supremum (union), proven without the Axiom of Regularity. (Contributed by Chen-Pang He, 1-Nov-2015)

	Ref	Expression
Assertion	ordtop	$$⊢\mathrm{Ord}J\to \left(J\in \mathrm{Top}\leftrightarrow J\ne \bigcup J\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\bigcup J=\bigcup J$$
2	1	topopn	$$⊢J\in \mathrm{Top}\to \bigcup J\in J$$
3		nordeq	$$⊢\left(\mathrm{Ord}J\wedge \bigcup J\in J\right)\to J\ne \bigcup J$$
4	3	ex	$$⊢\mathrm{Ord}J\to \left(\bigcup J\in J\to J\ne \bigcup J\right)$$
5	2 4	syl5	$$⊢\mathrm{Ord}J\to \left(J\in \mathrm{Top}\to J\ne \bigcup J\right)$$
6		onsuctop	$$⊢\bigcup J\in \mathrm{On}\to \mathrm{suc}\bigcup J\in \mathrm{Top}$$
7	6	ordtoplem	$$⊢\mathrm{Ord}J\to \left(J\ne \bigcup J\to J\in \mathrm{Top}\right)$$
8	5 7	impbid	$$⊢\mathrm{Ord}J\to \left(J\in \mathrm{Top}\leftrightarrow J\ne \bigcup J\right)$$