Theorem orduniss2

Description: The union of the ordinal subsets of an ordinal number is that number. (Contributed by NM, 30-Jan-2005)

	Ref	Expression
Assertion	orduniss2	|- ( Ord A -> U. { x e. On | x C_ A } = A )

Proof

Step	Hyp	Ref	Expression
1		df-rab	|- { x e. On | x C_ A } = { x | ( x e. On /\ x C_ A ) }
2		incom	|- ( { x | x e. On } i^i { x | x C_ A } ) = ( { x | x C_ A } i^i { x | x e. On } )
3		inab	|- ( { x | x e. On } i^i { x | x C_ A } ) = { x | ( x e. On /\ x C_ A ) }
4		df-pw	|- ~P A = { x | x C_ A }
5	4	eqcomi	|- { x | x C_ A } = ~P A
6		abid2	|- { x | x e. On } = On
7	5 6	ineq12i	|- ( { x | x C_ A } i^i { x | x e. On } ) = ( ~P A i^i On )
8	2 3 7	3eqtr3i	|- { x | ( x e. On /\ x C_ A ) } = ( ~P A i^i On )
9	1 8	eqtri	|- { x e. On | x C_ A } = ( ~P A i^i On )
10		ordpwsuc	|- ( Ord A -> ( ~P A i^i On ) = suc A )
11	9 10	syl5eq	|- ( Ord A -> { x e. On | x C_ A } = suc A )
12	11	unieqd	|- ( Ord A -> U. { x e. On | x C_ A } = U. suc A )
13		ordunisuc	|- ( Ord A -> U. suc A = A )
14	12 13	eqtrd	|- ( Ord A -> U. { x e. On | x C_ A } = A )