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

Proof

Step	Hyp	Ref	Expression
1		uniss	$$⊢A\subseteq \bigcup A\to \bigcup A\subseteq \bigcup \bigcup A$$
2		ssorduni	$$⊢A\subseteq \mathrm{On}\to \mathrm{Ord}\bigcup A$$
3		orduniss	$$⊢\mathrm{Ord}\bigcup A\to \bigcup \bigcup A\subseteq \bigcup A$$
4	2 3	syl	$$⊢A\subseteq \mathrm{On}\to \bigcup \bigcup A\subseteq \bigcup A$$
5	4	biantrud	$$⊢A\subseteq \mathrm{On}\to \left(\bigcup A\subseteq \bigcup \bigcup A\leftrightarrow \left(\bigcup A\subseteq \bigcup \bigcup A\wedge \bigcup \bigcup A\subseteq \bigcup A\right)\right)$$
6		eqss	$$⊢\bigcup A=\bigcup \bigcup A\leftrightarrow \left(\bigcup A\subseteq \bigcup \bigcup A\wedge \bigcup \bigcup A\subseteq \bigcup A\right)$$
7	5 6	bitr4di	$$⊢A\subseteq \mathrm{On}\to \left(\bigcup A\subseteq \bigcup \bigcup A\leftrightarrow \bigcup A=\bigcup \bigcup A\right)$$
8	1 7	imbitrid	$$⊢A\subseteq \mathrm{On}\to \left(A\subseteq \bigcup A\to \bigcup A=\bigcup \bigcup A\right)$$