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	|- ( Ord A -> U. suc A = A )

Proof

Step	Hyp	Ref	Expression
1		ordeleqon	|- ( Ord A <-> ( A e. On \/ A = On ) )
2		onunisuc	|- ( A e. On -> U. suc A = A )
3		sucon	|- suc On = On
4	3	unieqi	|- U. suc On = U. On
5		unon	|- U. On = On
6	4 5	eqtri	|- U. suc On = On
7		suceq	|- ( A = On -> suc A = suc On )
8	7	unieqd	|- ( A = On -> U. suc A = U. suc On )
9		id	|- ( A = On -> A = On )
10	6 8 9	3eqtr4a	|- ( A = On -> U. suc A = A )
11	2 10	jaoi	|- ( ( A e. On \/ A = On ) -> U. suc A = A )
12	1 11	sylbi	|- ( Ord A -> U. suc A = A )