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	|- ( Ord J -> ( J e. Top <-> J =/= U. J ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- U. J = U. J
2	1	topopn	|- ( J e. Top -> U. J e. J )
3		nordeq	|- ( ( Ord J /\ U. J e. J ) -> J =/= U. J )
4	3	ex	|- ( Ord J -> ( U. J e. J -> J =/= U. J ) )
5	2 4	syl5	|- ( Ord J -> ( J e. Top -> J =/= U. J ) )
6		onsuctop	|- ( U. J e. On -> suc U. J e. Top )
7	6	ordtoplem	|- ( Ord J -> ( J =/= U. J -> J e. Top ) )
8	5 7	impbid	|- ( Ord J -> ( J e. Top <-> J =/= U. J ) )