Theorem onsupsucismax

Description: If the union of a set of ordinals is a successor ordinal, then that union is the maximum element of the set. This is not a bijection because sets where the maximum element is zero or a limit ordinal exist. Lemma 2.11 of Schloeder p. 5. (Contributed by RP, 27-Jan-2025)

	Ref	Expression
Assertion	onsupsucismax	$$⊢\left(A\subseteq \mathrm{On}\wedge A\in V\right)\to \left(\exists b\in \mathrm{On}\bigcup A=\mathrm{suc}b\to \bigcup A\in A\right)$$

Proof

Step	Hyp	Ref	Expression
1		onsupnmax	$$⊢A\subseteq \mathrm{On}\to \left(\neg \bigcup A\in A\to \bigcup A=\bigcup \bigcup A\right)$$
2		ssorduni	$$⊢A\subseteq \mathrm{On}\to \mathrm{Ord}\bigcup A$$
3		orduninsuc	$$⊢\mathrm{Ord}\bigcup A\to \left(\bigcup A=\bigcup \bigcup A\leftrightarrow \neg \exists b\in \mathrm{On}\bigcup A=\mathrm{suc}b\right)$$
4	2 3	syl	$$⊢A\subseteq \mathrm{On}\to \left(\bigcup A=\bigcup \bigcup A\leftrightarrow \neg \exists b\in \mathrm{On}\bigcup A=\mathrm{suc}b\right)$$
5	1 4	sylibd	$$⊢A\subseteq \mathrm{On}\to \left(\neg \bigcup A\in A\to \neg \exists b\in \mathrm{On}\bigcup A=\mathrm{suc}b\right)$$
6	5	con4d	$$⊢A\subseteq \mathrm{On}\to \left(\exists b\in \mathrm{On}\bigcup A=\mathrm{suc}b\to \bigcup A\in A\right)$$
7	6	adantr	$$⊢\left(A\subseteq \mathrm{On}\wedge A\in V\right)\to \left(\exists b\in \mathrm{On}\bigcup A=\mathrm{suc}b\to \bigcup A\in A\right)$$