Theorem orduniorsuc

Description: An ordinal class is either its union or the successor of its union. If we adopt the view that zero is a limit ordinal, this means every ordinal class is either a limit or a successor. (Contributed by NM, 13-Sep-2003)

	Ref	Expression
Assertion	orduniorsuc	$$⊢\mathrm{Ord}A\to \left(A=\bigcup A\vee A=\mathrm{suc}\bigcup A\right)$$

Proof

Step	Hyp	Ref	Expression
1		orduniss	$$⊢\mathrm{Ord}A\to \bigcup A\subseteq A$$
2		orduni	$$⊢\mathrm{Ord}A\to \mathrm{Ord}\bigcup A$$
3		ordelssne	$$⊢\left(\mathrm{Ord}\bigcup A\wedge \mathrm{Ord}A\right)\to \left(\bigcup A\in A\leftrightarrow \left(\bigcup A\subseteq A\wedge \bigcup A\ne A\right)\right)$$
4	2 3	mpancom	$$⊢\mathrm{Ord}A\to \left(\bigcup A\in A\leftrightarrow \left(\bigcup A\subseteq A\wedge \bigcup A\ne A\right)\right)$$
5	4	biimprd	$$⊢\mathrm{Ord}A\to \left(\left(\bigcup A\subseteq A\wedge \bigcup A\ne A\right)\to \bigcup A\in A\right)$$
6	1 5	mpand	$$⊢\mathrm{Ord}A\to \left(\bigcup A\ne A\to \bigcup A\in A\right)$$
7		ordsucss	$$⊢\mathrm{Ord}A\to \left(\bigcup A\in A\to \mathrm{suc}\bigcup A\subseteq A\right)$$
8	6 7	syld	$$⊢\mathrm{Ord}A\to \left(\bigcup A\ne A\to \mathrm{suc}\bigcup A\subseteq A\right)$$
9		ordsucuni	$$⊢\mathrm{Ord}A\to A\subseteq \mathrm{suc}\bigcup A$$
10	8 9	jctild	$$⊢\mathrm{Ord}A\to \left(\bigcup A\ne A\to \left(A\subseteq \mathrm{suc}\bigcup A\wedge \mathrm{suc}\bigcup A\subseteq A\right)\right)$$
11		df-ne	$$⊢A\ne \bigcup A\leftrightarrow \neg A=\bigcup A$$
12		necom	$$⊢A\ne \bigcup A\leftrightarrow \bigcup A\ne A$$
13	11 12	bitr3i	$$⊢\neg A=\bigcup A\leftrightarrow \bigcup A\ne A$$
14		eqss	$$⊢A=\mathrm{suc}\bigcup A\leftrightarrow \left(A\subseteq \mathrm{suc}\bigcup A\wedge \mathrm{suc}\bigcup A\subseteq A\right)$$
15	10 13 14	3imtr4g	$$⊢\mathrm{Ord}A\to \left(\neg A=\bigcup A\to A=\mathrm{suc}\bigcup A\right)$$
16	15	orrd	$$⊢\mathrm{Ord}A\to \left(A=\bigcup A\vee A=\mathrm{suc}\bigcup A\right)$$