This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid 
 |-  ( 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 )