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	|- ( ( A e. On /\ A = suc B ) -> suc U. A = A )

Proof

Step	Hyp	Ref	Expression
1		eleq1	|- ( A = suc B -> ( A e. On <-> suc B e. On ) )
2	1	biimpac	|- ( ( A e. On /\ A = suc B ) -> suc B e. On )
3		eloni	|- ( suc B e. On -> Ord suc B )
4		ordsuc	|- ( Ord B <-> Ord suc B )
5		ordunisuc	|- ( Ord B -> U. suc B = B )
6	4 5	sylbir	|- ( Ord suc B -> U. suc B = B )
7		suceq	|- ( U. suc B = B -> suc U. suc B = suc B )
8	6 7	syl	|- ( Ord suc B -> suc U. suc B = suc B )
9		ordunisuc	|- ( Ord suc B -> U. suc suc B = suc B )
10	8 9	eqtr4d	|- ( Ord suc B -> suc U. suc B = U. suc suc B )
11	2 3 10	3syl	|- ( ( A e. On /\ A = suc B ) -> suc U. suc B = U. suc suc B )
12		unieq	|- ( A = suc B -> U. A = U. suc B )
13		suceq	|- ( U. A = U. suc B -> suc U. A = suc U. suc B )
14	12 13	syl	|- ( A = suc B -> suc U. A = suc U. suc B )
15		suceq	|- ( A = suc B -> suc A = suc suc B )
16	15	unieqd	|- ( A = suc B -> U. suc A = U. suc suc B )
17	14 16	eqeq12d	|- ( A = suc B -> ( suc U. A = U. suc A <-> suc U. suc B = U. suc suc B ) )
18	11 17	imbitrrid	|- ( A = suc B -> ( ( A e. On /\ A = suc B ) -> suc U. A = U. suc A ) )
19	18	anabsi7	|- ( ( A e. On /\ A = suc B ) -> suc U. A = U. suc A )
20		eloni	|- ( A e. On -> Ord A )
21		ordunisuc	|- ( Ord A -> U. suc A = A )
22	20 21	syl	|- ( A e. On -> U. suc A = A )
23	22	adantr	|- ( ( A e. On /\ A = suc B ) -> U. suc A = A )
24	19 23	eqtrd	|- ( ( A e. On /\ A = suc B ) -> suc U. A = A )