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

Theorem suceloni 4495
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 4327 . . . . . . . 8  |-  ( A  e.  On  ->  (
x  e.  A  ->  x  C_  A ) )
2 elsn 3559 . . . . . . . . . 10  |-  ( x  e.  { A }  <->  x  =  A )
3 eqimss 3151 . . . . . . . . . 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 4291 . . . . . . . . 9  |-  suc  A  =  ( A  u.  { A } )
87eleq2i 2317 . . . . . . . 8  |-  ( x  e.  suc  A  <->  x  e.  ( A  u.  { A } ) )
9 elun 3226 . . . . . . . 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 4362 . . . . . 6  |-  A  C_  suc  A
14 sstr2 3107 . . . . . 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 2587 . . . 4  |-  ( A  e.  On  ->  A. x  e.  suc  A x  C_  suc  A )
17 dftr3 4014 . . . 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 4473 . . . . 5  |-  ( A  e.  On  ->  A  C_  On )
20 snssi 3659 . . . . 5  |-  ( A  e.  On  ->  { A }  C_  On )
2119, 20unssd 3261 . . . 4  |-  ( A  e.  On  ->  ( A  u.  { A } )  C_  On )
227, 21syl5eqss 3143 . . 3  |-  ( A  e.  On  ->  suc  A 
C_  On )
23 ordon 4465 . . . 4  |-  Ord  On
24 trssord 4302 . . . . 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 4492 . . 3  |-  ( A  e.  On  ->  suc  A  e.  _V )
29 elong 4293 . . 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 2509   _Vcvv 2727    u. cun 3076    C_ wss 3078   {csn 3544   Tr wtr 4010   Ord word 4284   Oncon0 4285   suc csuc 4287
This theorem is referenced by:  ordsuc  4496  unon  4513  onsuci  4520  ordunisuc2  4526  ordzsl  4527  onzsl  4528  tfindsg  4542  dfom2  4549  findsg  4574  tfrlem12  6291  oasuc  6409  omsuc  6411  onasuc  6413  oacl  6420  oneo  6465  omeulem1  6466  omeulem2  6467  oeordi  6471  oeworde  6477  oelim2  6479  oelimcl  6484  oeeulem  6485  oeeui  6486  oaabs2  6529  omxpenlem  6848  card2inf  7153  cantnflt  7257  cantnflem1d  7274  cnfcom  7287  r1ordg  7334  bndrank  7397  r1pw  7401  r1pwOLD  7402  tcrank  7438  onssnum  7551  dfac12lem2  7654  cfsuc  7767  cfsmolem  7780  fin1a2lem1  7910  fin1a2lem2  7911  ttukeylem7  8026  alephreg  8084  gch2  8181  winainflem  8195  winalim2  8198  r1wunlim  8239  nqereu  8433  ontgval  24044  ontgsucval  24045  onsuctop  24046
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 1926  ax-ext 2234  ax-sep 4038  ax-nul 4046  ax-pr 4108  ax-un 4403
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 1883  df-eu 2118  df-mo 2119  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-ral 2513  df-rex 2514  df-rab 2516  df-v 2729  df-sbc 2922  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-pss 3091  df-nul 3363  df-if 3471  df-sn 3550  df-pr 3551  df-tp 3552  df-op 3553  df-uni 3728  df-br 3921  df-opab 3975  df-tr 4011  df-eprel 4198  df-po 4207  df-so 4208  df-fr 4245  df-we 4247  df-ord 4288  df-on 4289  df-suc 4291
  Copyright terms: Public domain W3C validator