Theorem onsupneqmaxlim0

Description: If the supremum of a class of ordinals is not in that class, then the supremum is a limit ordinal or empty. (Contributed by RP, 27-Jan-2025)

	Ref	Expression
Assertion	onsupneqmaxlim0	|- ( A C_ On -> ( A C_ U. A -> U. A = U. U. A ) )

Proof

Step	Hyp	Ref	Expression
1		uniss	|- ( A C_ U. A -> U. A C_ U. U. A )
2		ssorduni	|- ( A C_ On -> Ord U. A )
3		orduniss	|- ( Ord U. A -> U. U. A C_ U. A )
4	2 3	syl	|- ( A C_ On -> U. U. A C_ U. A )
5	4	biantrud	|- ( A C_ On -> ( U. A C_ U. U. A <-> ( U. A C_ U. U. A /\ U. U. A C_ U. A ) ) )
6		eqss	|- ( U. A = U. U. A <-> ( U. A C_ U. U. A /\ U. U. A C_ U. A ) )
7	5 6	bitr4di	|- ( A C_ On -> ( U. A C_ U. U. A <-> U. A = U. U. A ) )
8	1 7	imbitrid	|- ( A C_ On -> ( A C_ U. A -> U. A = U. U. A ) )