MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssorduni Unicode version

Theorem ssorduni 4578
Description: The union of a class of ordinal numbers is ordinal. Proposition 7.19 of [TakeutiZaring] p. 40. (Contributed by NM, 30-May-1994.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
Assertion
Ref Expression
ssorduni  |-  ( A 
C_  On  ->  Ord  U. A )
Dummy variables  x  y are mutually distinct and distinct from all other variables.

Proof of Theorem ssorduni
StepHypRef Expression
1 eluni2 3834 . . . . 5  |-  ( x  e.  U. A  <->  E. y  e.  A  x  e.  y )
2 ssel 3177 . . . . . . . . 9  |-  ( A 
C_  On  ->  ( y  e.  A  ->  y  e.  On ) )
3 onelss 4435 . . . . . . . . 9  |-  ( y  e.  On  ->  (
x  e.  y  ->  x  C_  y ) )
42, 3syl6 31 . . . . . . . 8  |-  ( A 
C_  On  ->  ( y  e.  A  ->  (
x  e.  y  ->  x  C_  y ) ) )
5 anc2r 541 . . . . . . . 8  |-  ( ( y  e.  A  -> 
( x  e.  y  ->  x  C_  y
) )  ->  (
y  e.  A  -> 
( x  e.  y  ->  ( x  C_  y  /\  y  e.  A
) ) ) )
64, 5syl 17 . . . . . . 7  |-  ( A 
C_  On  ->  ( y  e.  A  ->  (
x  e.  y  -> 
( x  C_  y  /\  y  e.  A
) ) ) )
7 ssuni 3852 . . . . . . 7  |-  ( ( x  C_  y  /\  y  e.  A )  ->  x  C_  U. A )
86, 7syl8 67 . . . . . 6  |-  ( A 
C_  On  ->  ( y  e.  A  ->  (
x  e.  y  ->  x  C_  U. A ) ) )
98rexlimdv 2669 . . . . 5  |-  ( A 
C_  On  ->  ( E. y  e.  A  x  e.  y  ->  x  C_ 
U. A ) )
101, 9syl5bi 210 . . . 4  |-  ( A 
C_  On  ->  ( x  e.  U. A  ->  x  C_  U. A ) )
1110ralrimiv 2628 . . 3  |-  ( A 
C_  On  ->  A. x  e.  U. A x  C_  U. A )
12 dftr3 4120 . . 3  |-  ( Tr 
U. A  <->  A. x  e.  U. A x  C_  U. A )
1311, 12sylibr 205 . 2  |-  ( A 
C_  On  ->  Tr  U. A )
14 onelon 4418 . . . . . . 7  |-  ( ( y  e.  On  /\  x  e.  y )  ->  x  e.  On )
1514ex 425 . . . . . 6  |-  ( y  e.  On  ->  (
x  e.  y  ->  x  e.  On )
)
162, 15syl6 31 . . . . 5  |-  ( A 
C_  On  ->  ( y  e.  A  ->  (
x  e.  y  ->  x  e.  On )
) )
1716rexlimdv 2669 . . . 4  |-  ( A 
C_  On  ->  ( E. y  e.  A  x  e.  y  ->  x  e.  On ) )
181, 17syl5bi 210 . . 3  |-  ( A 
C_  On  ->  ( x  e.  U. A  ->  x  e.  On )
)
1918ssrdv 3188 . 2  |-  ( A 
C_  On  ->  U. A  C_  On )
20 ordon 4575 . . 3  |-  Ord  On
21 trssord 4410 . . . 4  |-  ( ( Tr  U. A  /\  U. A  C_  On  /\  Ord  On )  ->  Ord  U. A
)
22213exp 1152 . . 3  |-  ( Tr 
U. A  ->  ( U. A  C_  On  ->  ( Ord  On  ->  Ord  U. A ) ) )
2320, 22mpii 41 . 2  |-  ( Tr 
U. A  ->  ( U. A  C_  On  ->  Ord  U. A ) )
2413, 19, 23sylc 58 1  |-  ( A 
C_  On  ->  Ord  U. A )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    e. wcel 1687   A.wral 2546   E.wrex 2547    C_ wss 3155   U.cuni 3830   Tr wtr 4116   Ord word 4392   Oncon0 4393
This theorem is referenced by:  ssonuni  4579  ssonprc  4584  orduni  4586  onsucuni  4620  limuni3  4644  onfununi  6355  tfrlem8  6397  onssnum  7664  unialeph  7725  cfslbn  7890  hsmexlem1  8049  inaprc  8455  axfelem1  23749  axfelem2  23750
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1638  ax-8 1646  ax-13 1689  ax-14 1691  ax-6 1706  ax-7 1711  ax-11 1718  ax-12 1870  ax-ext 2267  ax-sep 4144  ax-nul 4152  ax-pr 4215  ax-un 4513
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 937  df-3an 938  df-tru 1312  df-ex 1531  df-nf 1534  df-sb 1633  df-eu 2150  df-mo 2151  df-clab 2273  df-cleq 2279  df-clel 2282  df-nfc 2411  df-ne 2451  df-ral 2551  df-rex 2552  df-rab 2555  df-v 2793  df-sbc 2995  df-dif 3158  df-un 3160  df-in 3162  df-ss 3169  df-pss 3171  df-nul 3459  df-if 3569  df-sn 3649  df-pr 3650  df-tp 3651  df-op 3652  df-uni 3831  df-br 4027  df-opab 4081  df-tr 4117  df-eprel 4306  df-po 4315  df-so 4316  df-fr 4353  df-we 4355  df-ord 4396  df-on 4397
  Copyright terms: Public domain W3C validator