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

Theorem suceloni 6443
Description: The successor of an ordinal number is an ordinal number. Proposition 7.24 of [TakeutiZaring] p. 41. (Contributed by NM, 6-Jun-1994.)
Assertion
Ref Expression
suceloni  |-  ( A  e.  On  ->  suc  A  e.  On )

Proof of Theorem suceloni
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 onelss 4780 . . . . . . . 8  |-  ( A  e.  On  ->  (
x  e.  A  ->  x  C_  A ) )
2 elsn 3910 . . . . . . . . . 10  |-  ( x  e.  { A }  <->  x  =  A )
3 eqimss 3427 . . . . . . . . . 10  |-  ( x  =  A  ->  x  C_  A )
42, 3sylbi 195 . . . . . . . . 9  |-  ( x  e.  { A }  ->  x  C_  A )
54a1i 11 . . . . . . . 8  |-  ( A  e.  On  ->  (
x  e.  { A }  ->  x  C_  A
) )
61, 5orim12d 834 . . . . . . 7  |-  ( A  e.  On  ->  (
( x  e.  A  \/  x  e.  { A } )  ->  (
x  C_  A  \/  x  C_  A ) ) )
7 df-suc 4744 . . . . . . . . 9  |-  suc  A  =  ( A  u.  { A } )
87eleq2i 2507 . . . . . . . 8  |-  ( x  e.  suc  A  <->  x  e.  ( A  u.  { A } ) )
9 elun 3516 . . . . . . . 8  |-  ( x  e.  ( A  u.  { A } )  <->  ( x  e.  A  \/  x  e.  { A } ) )
108, 9bitr2i 250 . . . . . . 7  |-  ( ( x  e.  A  \/  x  e.  { A } )  <->  x  e.  suc  A )
11 oridm 514 . . . . . . 7  |-  ( ( x  C_  A  \/  x  C_  A )  <->  x  C_  A
)
126, 10, 113imtr3g 269 . . . . . 6  |-  ( A  e.  On  ->  (
x  e.  suc  A  ->  x  C_  A )
)
13 sssucid 4815 . . . . . 6  |-  A  C_  suc  A
14 sstr2 3382 . . . . . 6  |-  ( x 
C_  A  ->  ( A  C_  suc  A  ->  x  C_  suc  A ) )
1512, 13, 14syl6mpi 62 . . . . 5  |-  ( A  e.  On  ->  (
x  e.  suc  A  ->  x  C_  suc  A ) )
1615ralrimiv 2817 . . . 4  |-  ( A  e.  On  ->  A. x  e.  suc  A x  C_  suc  A )
17 dftr3 4408 . . . 4  |-  ( Tr 
suc  A  <->  A. x  e.  suc  A x  C_  suc  A )
1816, 17sylibr 212 . . 3  |-  ( A  e.  On  ->  Tr  suc  A )
19 onss 6421 . . . . 5  |-  ( A  e.  On  ->  A  C_  On )
20 snssi 4036 . . . . 5  |-  ( A  e.  On  ->  { A }  C_  On )
2119, 20unssd 3551 . . . 4  |-  ( A  e.  On  ->  ( A  u.  { A } )  C_  On )
227, 21syl5eqss 3419 . . 3  |-  ( A  e.  On  ->  suc  A 
C_  On )
23 ordon 6413 . . . 4  |-  Ord  On
24 trssord 4755 . . . . 5  |-  ( ( Tr  suc  A  /\  suc  A  C_  On  /\  Ord  On )  ->  Ord  suc  A
)
25243exp 1186 . . . 4  |-  ( Tr 
suc  A  ->  ( suc 
A  C_  On  ->  ( Ord  On  ->  Ord  suc 
A ) ) )
2623, 25mpii 43 . . 3  |-  ( Tr 
suc  A  ->  ( suc 
A  C_  On  ->  Ord 
suc  A ) )
2718, 22, 26sylc 60 . 2  |-  ( A  e.  On  ->  Ord  suc 
A )
28 sucexg 6440 . . 3  |-  ( A  e.  On  ->  suc  A  e.  _V )
29 elong 4746 . . 3  |-  ( suc 
A  e.  _V  ->  ( suc  A  e.  On  <->  Ord 
suc  A ) )
3028, 29syl 16 . 2  |-  ( A  e.  On  ->  ( suc  A  e.  On  <->  Ord  suc  A
) )
3127, 30mpbird 232 1  |-  ( A  e.  On  ->  suc  A  e.  On )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    \/ wo 368    = wceq 1369    e. wcel 1756   A.wral 2734   _Vcvv 2991    u. cun 3345    C_ wss 3347   {csn 3896   Tr wtr 4404   Ord word 4737   Oncon0 4738   suc csuc 4740
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4432  ax-nul 4440  ax-pr 4550  ax-un 6391
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2739  df-rex 2740  df-rab 2743  df-v 2993  df-sbc 3206  df-dif 3350  df-un 3352  df-in 3354  df-ss 3361  df-pss 3363  df-nul 3657  df-if 3811  df-sn 3897  df-pr 3899  df-tp 3901  df-op 3903  df-uni 4111  df-br 4312  df-opab 4370  df-tr 4405  df-eprel 4651  df-po 4660  df-so 4661  df-fr 4698  df-we 4700  df-ord 4741  df-on 4742  df-suc 4744
This theorem is referenced by:  ordsuc  6444  unon  6461  onsuci  6468  ordunisuc2  6474  ordzsl  6475  onzsl  6476  tfindsg  6490  dfom2  6497  findsg  6522  tfrlem12  6867  oasuc  6983  omsuc  6985  onasuc  6987  oacl  6994  oneo  7039  omeulem1  7040  omeulem2  7041  oeordi  7045  oeworde  7051  oelim2  7053  oelimcl  7058  oeeulem  7059  oeeui  7060  oaabs2  7103  omxpenlem  7431  card2inf  7789  cantnflt  7899  cantnflem1d  7915  cantnfltOLD  7929  cantnflem1dOLD  7938  cnfcom  7952  cnfcomOLD  7960  r1ordg  8004  bndrank  8067  r1pw  8071  r1pwOLD  8072  tcrank  8110  onssnum  8229  dfac12lem2  8332  cfsuc  8445  cfsmolem  8458  fin1a2lem1  8588  fin1a2lem2  8589  ttukeylem7  8703  alephreg  8765  gch2  8861  winainflem  8879  winalim2  8882  r1wunlim  8923  nqereu  9117  ontgval  28296  ontgsucval  28297  onsuctop  28298
  Copyright terms: Public domain W3C validator