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

Theorem suceloni 4760
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 4591 . . . . . . . 8  |-  ( A  e.  On  ->  (
x  e.  A  ->  x  C_  A ) )
2 elsn 3797 . . . . . . . . . 10  |-  ( x  e.  { A }  <->  x  =  A )
3 eqimss 3368 . . . . . . . . . 10  |-  ( x  =  A  ->  x  C_  A )
42, 3sylbi 188 . . . . . . . . 9  |-  ( x  e.  { A }  ->  x  C_  A )
54a1i 11 . . . . . . . 8  |-  ( A  e.  On  ->  (
x  e.  { A }  ->  x  C_  A
) )
61, 5orim12d 812 . . . . . . 7  |-  ( A  e.  On  ->  (
( x  e.  A  \/  x  e.  { A } )  ->  (
x  C_  A  \/  x  C_  A ) ) )
7 df-suc 4555 . . . . . . . . 9  |-  suc  A  =  ( A  u.  { A } )
87eleq2i 2476 . . . . . . . 8  |-  ( x  e.  suc  A  <->  x  e.  ( A  u.  { A } ) )
9 elun 3456 . . . . . . . 8  |-  ( x  e.  ( A  u.  { A } )  <->  ( x  e.  A  \/  x  e.  { A } ) )
108, 9bitr2i 242 . . . . . . 7  |-  ( ( x  e.  A  \/  x  e.  { A } )  <->  x  e.  suc  A )
11 oridm 501 . . . . . . 7  |-  ( ( x  C_  A  \/  x  C_  A )  <->  x  C_  A
)
126, 10, 113imtr3g 261 . . . . . 6  |-  ( A  e.  On  ->  (
x  e.  suc  A  ->  x  C_  A )
)
13 sssucid 4626 . . . . . 6  |-  A  C_  suc  A
14 sstr2 3323 . . . . . 6  |-  ( x 
C_  A  ->  ( A  C_  suc  A  ->  x  C_  suc  A ) )
1512, 13, 14syl6mpi 60 . . . . 5  |-  ( A  e.  On  ->  (
x  e.  suc  A  ->  x  C_  suc  A ) )
1615ralrimiv 2756 . . . 4  |-  ( A  e.  On  ->  A. x  e.  suc  A x  C_  suc  A )
17 dftr3 4274 . . . 4  |-  ( Tr 
suc  A  <->  A. x  e.  suc  A x  C_  suc  A )
1816, 17sylibr 204 . . 3  |-  ( A  e.  On  ->  Tr  suc  A )
19 onss 4738 . . . . 5  |-  ( A  e.  On  ->  A  C_  On )
20 snssi 3910 . . . . 5  |-  ( A  e.  On  ->  { A }  C_  On )
2119, 20unssd 3491 . . . 4  |-  ( A  e.  On  ->  ( A  u.  { A } )  C_  On )
227, 21syl5eqss 3360 . . 3  |-  ( A  e.  On  ->  suc  A 
C_  On )
23 ordon 4730 . . . 4  |-  Ord  On
24 trssord 4566 . . . . 5  |-  ( ( Tr  suc  A  /\  suc  A  C_  On  /\  Ord  On )  ->  Ord  suc  A
)
25243exp 1152 . . . 4  |-  ( Tr 
suc  A  ->  ( suc 
A  C_  On  ->  ( Ord  On  ->  Ord  suc 
A ) ) )
2623, 25mpii 41 . . 3  |-  ( Tr 
suc  A  ->  ( suc 
A  C_  On  ->  Ord 
suc  A ) )
2718, 22, 26sylc 58 . 2  |-  ( A  e.  On  ->  Ord  suc 
A )
28 sucexg 4757 . . 3  |-  ( A  e.  On  ->  suc  A  e.  _V )
29 elong 4557 . . 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 224 1  |-  ( A  e.  On  ->  suc  A  e.  On )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    \/ wo 358    = wceq 1649    e. wcel 1721   A.wral 2674   _Vcvv 2924    u. cun 3286    C_ wss 3288   {csn 3782   Tr wtr 4270   Ord word 4548   Oncon0 4549   suc csuc 4551
This theorem is referenced by:  ordsuc  4761  unon  4778  onsuci  4785  ordunisuc2  4791  ordzsl  4792  onzsl  4793  tfindsg  4807  dfom2  4814  findsg  4839  tfrlem12  6617  oasuc  6735  omsuc  6737  onasuc  6739  oacl  6746  oneo  6791  omeulem1  6792  omeulem2  6793  oeordi  6797  oeworde  6803  oelim2  6805  oelimcl  6810  oeeulem  6811  oeeui  6812  oaabs2  6855  omxpenlem  7176  card2inf  7487  cantnflt  7591  cantnflem1d  7608  cnfcom  7621  r1ordg  7668  bndrank  7731  r1pw  7735  r1pwOLD  7736  tcrank  7772  onssnum  7885  dfac12lem2  7988  cfsuc  8101  cfsmolem  8114  fin1a2lem1  8244  fin1a2lem2  8245  ttukeylem7  8359  alephreg  8421  gch2  8518  winainflem  8532  winalim2  8535  r1wunlim  8576  nqereu  8770  ontgval  26093  ontgsucval  26094  onsuctop  26095
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-sep 4298  ax-nul 4306  ax-pr 4371  ax-un 4668
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-ral 2679  df-rex 2680  df-rab 2683  df-v 2926  df-sbc 3130  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-pss 3304  df-nul 3597  df-if 3708  df-sn 3788  df-pr 3789  df-tp 3790  df-op 3791  df-uni 3984  df-br 4181  df-opab 4235  df-tr 4271  df-eprel 4462  df-po 4471  df-so 4472  df-fr 4509  df-we 4511  df-ord 4552  df-on 4553  df-suc 4555
  Copyright terms: Public domain W3C validator