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

Metamath Proof Explorer

Theorem ssorduni

Description: The union of a class of ordinal numbers is ordinal. Proposition 7.19 of TakeutiZaring p. 40. Lemma 2.7 of Schloeder p. 4. (Contributed by NM, 30-May-1994) (Proof shortened by Andrew Salmon, 12-Aug-2011)

Ref Expression
Assertion ssorduni 
|- ( A C_ On -> Ord U. A )

Proof

Step Hyp Ref Expression
1 eluni2 
 |-  ( x e. U. A <-> E. y e. A x e. y )
2 ssel 
 |-  ( A C_ On -> ( y e. A -> y e. On ) )
3 onelss 
 |-  ( y e. On -> ( x e. y -> x C_ y ) )
4 2 3 syl6 
 |-  ( A C_ On -> ( y e. A -> ( x e. y -> x C_ y ) ) )
5 anc2r 
 |-  ( ( y e. A -> ( x e. y -> x C_ y ) ) -> ( y e. A -> ( x e. y -> ( x C_ y /\ y e. A ) ) ) )
6 4 5 syl 
 |-  ( A C_ On -> ( y e. A -> ( x e. y -> ( x C_ y /\ y e. A ) ) ) )
7 ssuni 
 |-  ( ( x C_ y /\ y e. A ) -> x C_ U. A )
8 6 7 syl8 
 |-  ( A C_ On -> ( y e. A -> ( x e. y -> x C_ U. A ) ) )
9 8 rexlimdv 
 |-  ( A C_ On -> ( E. y e. A x e. y -> x C_ U. A ) )
10 1 9 biimtrid 
 |-  ( A C_ On -> ( x e. U. A -> x C_ U. A ) )
11 10 ralrimiv 
 |-  ( A C_ On -> A. x e. U. A x C_ U. A )
12 dftr3 
 |-  ( Tr U. A <-> A. x e. U. A x C_ U. A )
13 11 12 sylibr 
 |-  ( A C_ On -> Tr U. A )
14 onelon 
 |-  ( ( y e. On /\ x e. y ) -> x e. On )
15 14 ex 
 |-  ( y e. On -> ( x e. y -> x e. On ) )
16 2 15 syl6 
 |-  ( A C_ On -> ( y e. A -> ( x e. y -> x e. On ) ) )
17 16 rexlimdv 
 |-  ( A C_ On -> ( E. y e. A x e. y -> x e. On ) )
18 1 17 biimtrid 
 |-  ( A C_ On -> ( x e. U. A -> x e. On ) )
19 18 ssrdv 
 |-  ( A C_ On -> U. A C_ On )
20 ordon 
 |-  Ord On
21 trssord 
 |-  ( ( Tr U. A /\ U. A C_ On /\ Ord On ) -> Ord U. A )
22 21 3exp 
 |-  ( Tr U. A -> ( U. A C_ On -> ( Ord On -> Ord U. A ) ) )
23 20 22 mpii 
 |-  ( Tr U. A -> ( U. A C_ On -> Ord U. A ) )
24 13 19 23 sylc 
 |-  ( A C_ On -> Ord U. A )