Theorem ordunisuc

Description: An ordinal class is equal to the union of its successor. (Contributed by NM, 10-Dec-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011)

	Ref	Expression
Assertion	ordunisuc	$$⊢\mathrm{Ord}A\to \bigcup \mathrm{suc}A=A$$

Proof

Step	Hyp	Ref	Expression
1		ordeleqon	$$⊢\mathrm{Ord}A\leftrightarrow \left(A\in \mathrm{On}\vee A=\mathrm{On}\right)$$
2		onunisuc	$$⊢A\in \mathrm{On}\to \bigcup \mathrm{suc}A=A$$
3		sucon	$$⊢\mathrm{suc}\mathrm{On}=\mathrm{On}$$
4	3	unieqi	$$⊢\bigcup \mathrm{suc}\mathrm{On}=\bigcup \mathrm{On}$$
5		unon	$$⊢\bigcup \mathrm{On}=\mathrm{On}$$
6	4 5	eqtri	$$⊢\bigcup \mathrm{suc}\mathrm{On}=\mathrm{On}$$
7		suceq	$$⊢A=\mathrm{On}\to \mathrm{suc}A=\mathrm{suc}\mathrm{On}$$
8	7	unieqd	$$⊢A=\mathrm{On}\to \bigcup \mathrm{suc}A=\bigcup \mathrm{suc}\mathrm{On}$$
9		id	$$⊢A=\mathrm{On}\to A=\mathrm{On}$$
10	6 8 9	3eqtr4a	$$⊢A=\mathrm{On}\to \bigcup \mathrm{suc}A=A$$
11	2 10	jaoi	$$⊢\left(A\in \mathrm{On}\vee A=\mathrm{On}\right)\to \bigcup \mathrm{suc}A=A$$
12	1 11	sylbi	$$⊢\mathrm{Ord}A\to \bigcup \mathrm{suc}A=A$$