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

Theorem suceloni 4562
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
StepHypRef Expression
1 onelss 4392 . . . . . . . 8  |-  ( A  e.  On  ->  (
x  e.  A  ->  x  C_  A ) )
2 elsn 3615 . . . . . . . . . 10  |-  ( x  e.  { A }  <->  x  =  A )
3 eqimss 3191 . . . . . . . . . 10  |-  ( x  =  A  ->  x  C_  A )
42, 3sylbi 189 . . . . . . . . 9  |-  ( x  e.  { A }  ->  x  C_  A )
54a1i 12 . . . . . . . 8  |-  ( A  e.  On  ->  (
x  e.  { A }  ->  x  C_  A
) )
61, 5orim12d 814 . . . . . . 7  |-  ( A  e.  On  ->  (
( x  e.  A  \/  x  e.  { A } )  ->  (
x  C_  A  \/  x  C_  A ) ) )
7 df-suc 4356 . . . . . . . . 9  |-  suc  A  =  ( A  u.  { A } )
87eleq2i 2320 . . . . . . . 8  |-  ( x  e.  suc  A  <->  x  e.  ( A  u.  { A } ) )
9 elun 3277 . . . . . . . 8  |-  ( x  e.  ( A  u.  { A } )  <->  ( x  e.  A  \/  x  e.  { A } ) )
108, 9bitr2i 243 . . . . . . 7  |-  ( ( x  e.  A  \/  x  e.  { A } )  <->  x  e.  suc  A )
11 oridm 502 . . . . . . 7  |-  ( ( x  C_  A  \/  x  C_  A )  <->  x  C_  A
)
126, 10, 113imtr3g 262 . . . . . 6  |-  ( A  e.  On  ->  (
x  e.  suc  A  ->  x  C_  A )
)
13 sssucid 4427 . . . . . 6  |-  A  C_  suc  A
14 sstr2 3147 . . . . . 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 2598 . . . 4  |-  ( A  e.  On  ->  A. x  e.  suc  A x  C_  suc  A )
17 dftr3 4077 . . . 4  |-  ( Tr 
suc  A  <->  A. x  e.  suc  A x  C_  suc  A )
1816, 17sylibr 205 . . 3  |-  ( A  e.  On  ->  Tr  suc  A )
19 onss 4540 . . . . 5  |-  ( A  e.  On  ->  A  C_  On )
20 snssi 3719 . . . . 5  |-  ( A  e.  On  ->  { A }  C_  On )
2119, 20unssd 3312 . . . 4  |-  ( A  e.  On  ->  ( A  u.  { A } )  C_  On )
227, 21syl5eqss 3183 . . 3  |-  ( A  e.  On  ->  suc  A 
C_  On )
23 ordon 4532 . . . 4  |-  Ord  On
24 trssord 4367 . . . . 5  |-  ( ( Tr  suc  A  /\  suc  A  C_  On  /\  Ord  On )  ->  Ord  suc  A
)
25243exp 1155 . . . 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 4559 . . 3  |-  ( A  e.  On  ->  suc  A  e.  _V )
29 elong 4358 . . 3  |-  ( suc 
A  e.  _V  ->  ( suc  A  e.  On  <->  Ord 
suc  A ) )
3028, 29syl 17 . 2  |-  ( A  e.  On  ->  ( suc  A  e.  On  <->  Ord  suc  A
) )
3127, 30mpbird 225 1  |-  ( A  e.  On  ->  suc  A  e.  On )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    \/ wo 359    = wceq 1619    e. wcel 1621   A.wral 2516   _Vcvv 2757    u. cun 3111    C_ wss 3113   {csn 3600   Tr wtr 4073   Ord word 4349   Oncon0 4350   suc csuc 4352
This theorem is referenced by:  ordsuc  4563  unon  4580  onsuci  4587  ordunisuc2  4593  ordzsl  4594  onzsl  4595  tfindsg  4609  dfom2  4616  findsg  4641  tfrlem12  6359  oasuc  6477  omsuc  6479  onasuc  6481  oacl  6488  oneo  6533  omeulem1  6534  omeulem2  6535  oeordi  6539  oeworde  6545  oelim2  6547  oelimcl  6552  oeeulem  6553  oeeui  6554  oaabs2  6597  omxpenlem  6917  card2inf  7223  cantnflt  7327  cantnflem1d  7344  cnfcom  7357  r1ordg  7404  bndrank  7467  r1pw  7471  r1pwOLD  7472  tcrank  7508  onssnum  7621  dfac12lem2  7724  cfsuc  7837  cfsmolem  7850  fin1a2lem1  7980  fin1a2lem2  7981  ttukeylem7  8096  alephreg  8158  gch2  8255  winainflem  8269  winalim2  8272  r1wunlim  8313  nqereu  8507  ontgval  24231  ontgsucval  24232  onsuctop  24233
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-sep 4101  ax-nul 4109  ax-pr 4172  ax-un 4470
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2121  df-mo 2122  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-ral 2521  df-rex 2522  df-rab 2525  df-v 2759  df-sbc 2953  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-pss 3129  df-nul 3417  df-if 3526  df-sn 3606  df-pr 3607  df-tp 3608  df-op 3609  df-uni 3788  df-br 3984  df-opab 4038  df-tr 4074  df-eprel 4263  df-po 4272  df-so 4273  df-fr 4310  df-we 4312  df-ord 4353  df-on 4354  df-suc 4356
  Copyright terms: Public domain W3C validator