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		suceq	$$⊢x=A\to \mathrm{suc}x=\mathrm{suc}A$$
3	2	unieqd	$$⊢x=A\to \bigcup \mathrm{suc}x=\bigcup \mathrm{suc}A$$
4		id	$$⊢x=A\to x=A$$
5	3 4	eqeq12d	$$⊢x=A\to \left(\bigcup \mathrm{suc}x=x\leftrightarrow \bigcup \mathrm{suc}A=A\right)$$
6		eloni	$$⊢x\in \mathrm{On}\to \mathrm{Ord}x$$
7		ordtr	$$⊢\mathrm{Ord}x\to \mathrm{Tr}x$$
8	6 7	syl	$$⊢x\in \mathrm{On}\to \mathrm{Tr}x$$
9		vex	$$⊢x\in \mathrm{V}$$
10	9	unisuc	$$⊢\mathrm{Tr}x\leftrightarrow \bigcup \mathrm{suc}x=x$$
11	8 10	sylib	$$⊢x\in \mathrm{On}\to \bigcup \mathrm{suc}x=x$$
12	5 11	vtoclga	$$⊢A\in \mathrm{On}\to \bigcup \mathrm{suc}A=A$$
13		sucon	$$⊢\mathrm{suc}\mathrm{On}=\mathrm{On}$$
14	13	unieqi	$$⊢\bigcup \mathrm{suc}\mathrm{On}=\bigcup \mathrm{On}$$
15		unon	$$⊢\bigcup \mathrm{On}=\mathrm{On}$$
16	14 15	eqtri	$$⊢\bigcup \mathrm{suc}\mathrm{On}=\mathrm{On}$$
17		suceq	$$⊢A=\mathrm{On}\to \mathrm{suc}A=\mathrm{suc}\mathrm{On}$$
18	17	unieqd	$$⊢A=\mathrm{On}\to \bigcup \mathrm{suc}A=\bigcup \mathrm{suc}\mathrm{On}$$
19		id	$$⊢A=\mathrm{On}\to A=\mathrm{On}$$
20	16 18 19	3eqtr4a	$$⊢A=\mathrm{On}\to \bigcup \mathrm{suc}A=A$$
21	12 20	jaoi	$$⊢\left(A\in \mathrm{On}\vee A=\mathrm{On}\right)\to \bigcup \mathrm{suc}A=A$$
22	1 21	sylbi	$$⊢\mathrm{Ord}A\to \bigcup \mathrm{suc}A=A$$