Theorem unizlim

Description: An ordinal equal to its own union is either zero or a limit ordinal. (Contributed by NM, 1-Oct-2003)

	Ref	Expression
Assertion	unizlim	$$⊢\mathrm{Ord}A\to \left(A=\bigcup A\leftrightarrow \left(A=\varnothing \vee \mathrm{Lim}A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-ne	$$⊢A\ne \varnothing \leftrightarrow \neg A=\varnothing$$
2		df-lim	$$⊢\mathrm{Lim}A\leftrightarrow \left(\mathrm{Ord}A\wedge A\ne \varnothing \wedge A=\bigcup A\right)$$
3	2	biimpri	$$⊢\left(\mathrm{Ord}A\wedge A\ne \varnothing \wedge A=\bigcup A\right)\to \mathrm{Lim}A$$
4	3	3exp	$$⊢\mathrm{Ord}A\to \left(A\ne \varnothing \to \left(A=\bigcup A\to \mathrm{Lim}A\right)\right)$$
5	1 4	syl5bir	$$⊢\mathrm{Ord}A\to \left(\neg A=\varnothing \to \left(A=\bigcup A\to \mathrm{Lim}A\right)\right)$$
6	5	com23	$$⊢\mathrm{Ord}A\to \left(A=\bigcup A\to \left(\neg A=\varnothing \to \mathrm{Lim}A\right)\right)$$
7	6	imp	$$⊢\left(\mathrm{Ord}A\wedge A=\bigcup A\right)\to \left(\neg A=\varnothing \to \mathrm{Lim}A\right)$$
8	7	orrd	$$⊢\left(\mathrm{Ord}A\wedge A=\bigcup A\right)\to \left(A=\varnothing \vee \mathrm{Lim}A\right)$$
9	8	ex	$$⊢\mathrm{Ord}A\to \left(A=\bigcup A\to \left(A=\varnothing \vee \mathrm{Lim}A\right)\right)$$
10		uni0	$$⊢\bigcup \varnothing =\varnothing$$
11	10	eqcomi	$$⊢\varnothing =\bigcup \varnothing$$
12		id	$$⊢A=\varnothing \to A=\varnothing$$
13		unieq	$$⊢A=\varnothing \to \bigcup A=\bigcup \varnothing$$
14	11 12 13	3eqtr4a	$$⊢A=\varnothing \to A=\bigcup A$$
15		limuni	$$⊢\mathrm{Lim}A\to A=\bigcup A$$
16	14 15	jaoi	$$⊢\left(A=\varnothing \vee \mathrm{Lim}A\right)\to A=\bigcup A$$
17	9 16	impbid1	$$⊢\mathrm{Ord}A\to \left(A=\bigcup A\leftrightarrow \left(A=\varnothing \vee \mathrm{Lim}A\right)\right)$$