Theorem onsucuni2

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

	Ref	Expression
Assertion	onsucuni2	$$⊢\left(A\in \mathrm{On}\wedge A=\mathrm{suc}B\right)\to \mathrm{suc}\bigcup A=A$$

Proof

Step	Hyp	Ref	Expression
1		eleq1	$$⊢A=\mathrm{suc}B\to \left(A\in \mathrm{On}\leftrightarrow \mathrm{suc}B\in \mathrm{On}\right)$$
2	1	biimpac	$$⊢\left(A\in \mathrm{On}\wedge A=\mathrm{suc}B\right)\to \mathrm{suc}B\in \mathrm{On}$$
3		eloni	$$⊢\mathrm{suc}B\in \mathrm{On}\to \mathrm{Ord}\mathrm{suc}B$$
4		ordsuc	$$⊢\mathrm{Ord}B\leftrightarrow \mathrm{Ord}\mathrm{suc}B$$
5		ordunisuc	$$⊢\mathrm{Ord}B\to \bigcup \mathrm{suc}B=B$$
6	4 5	sylbir	$$⊢\mathrm{Ord}\mathrm{suc}B\to \bigcup \mathrm{suc}B=B$$
7		suceq	$$⊢\bigcup \mathrm{suc}B=B\to \mathrm{suc}\bigcup \mathrm{suc}B=\mathrm{suc}B$$
8	6 7	syl	$$⊢\mathrm{Ord}\mathrm{suc}B\to \mathrm{suc}\bigcup \mathrm{suc}B=\mathrm{suc}B$$
9		ordunisuc	$$⊢\mathrm{Ord}\mathrm{suc}B\to \bigcup \mathrm{suc}\mathrm{suc}B=\mathrm{suc}B$$
10	8 9	eqtr4d	$$⊢\mathrm{Ord}\mathrm{suc}B\to \mathrm{suc}\bigcup \mathrm{suc}B=\bigcup \mathrm{suc}\mathrm{suc}B$$
11	2 3 10	3syl	$$⊢\left(A\in \mathrm{On}\wedge A=\mathrm{suc}B\right)\to \mathrm{suc}\bigcup \mathrm{suc}B=\bigcup \mathrm{suc}\mathrm{suc}B$$
12		unieq	$$⊢A=\mathrm{suc}B\to \bigcup A=\bigcup \mathrm{suc}B$$
13		suceq	$$⊢\bigcup A=\bigcup \mathrm{suc}B\to \mathrm{suc}\bigcup A=\mathrm{suc}\bigcup \mathrm{suc}B$$
14	12 13	syl	$$⊢A=\mathrm{suc}B\to \mathrm{suc}\bigcup A=\mathrm{suc}\bigcup \mathrm{suc}B$$
15		suceq	$$⊢A=\mathrm{suc}B\to \mathrm{suc}A=\mathrm{suc}\mathrm{suc}B$$
16	15	unieqd	$$⊢A=\mathrm{suc}B\to \bigcup \mathrm{suc}A=\bigcup \mathrm{suc}\mathrm{suc}B$$
17	14 16	eqeq12d	$$⊢A=\mathrm{suc}B\to \left(\mathrm{suc}\bigcup A=\bigcup \mathrm{suc}A\leftrightarrow \mathrm{suc}\bigcup \mathrm{suc}B=\bigcup \mathrm{suc}\mathrm{suc}B\right)$$
18	11 17	imbitrrid	$$⊢A=\mathrm{suc}B\to \left(\left(A\in \mathrm{On}\wedge A=\mathrm{suc}B\right)\to \mathrm{suc}\bigcup A=\bigcup \mathrm{suc}A\right)$$
19	18	anabsi7	$$⊢\left(A\in \mathrm{On}\wedge A=\mathrm{suc}B\right)\to \mathrm{suc}\bigcup A=\bigcup \mathrm{suc}A$$
20		eloni	$$⊢A\in \mathrm{On}\to \mathrm{Ord}A$$
21		ordunisuc	$$⊢\mathrm{Ord}A\to \bigcup \mathrm{suc}A=A$$
22	20 21	syl	$$⊢A\in \mathrm{On}\to \bigcup \mathrm{suc}A=A$$
23	22	adantr	$$⊢\left(A\in \mathrm{On}\wedge A=\mathrm{suc}B\right)\to \bigcup \mathrm{suc}A=A$$
24	19 23	eqtrd	$$⊢\left(A\in \mathrm{On}\wedge A=\mathrm{suc}B\right)\to \mathrm{suc}\bigcup A=A$$