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

Theorem limsuc 6629
Description: The successor of a member of a limit ordinal is also a member. (Contributed by NM, 3-Sep-2003.)
Assertion
Ref Expression
limsuc  |-  ( Lim 
A  ->  ( B  e.  A  <->  suc  B  e.  A
) )

Proof of Theorem limsuc
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 dflim4 6628 . . 3  |-  ( Lim 
A  <->  ( Ord  A  /\  (/)  e.  A  /\  A. x  e.  A  suc  x  e.  A )
)
2 suceq 5445 . . . . . 6  |-  ( x  =  B  ->  suc  x  =  suc  B )
32eleq1d 2485 . . . . 5  |-  ( x  =  B  ->  ( suc  x  e.  A  <->  suc  B  e.  A ) )
43rspccv 3117 . . . 4  |-  ( A. x  e.  A  suc  x  e.  A  ->  ( B  e.  A  ->  suc  B  e.  A ) )
543ad2ant3 1028 . . 3  |-  ( ( Ord  A  /\  (/)  e.  A  /\  A. x  e.  A  suc  x  e.  A )  ->  ( B  e.  A  ->  suc  B  e.  A ) )
61, 5sylbi 198 . 2  |-  ( Lim 
A  ->  ( B  e.  A  ->  suc  B  e.  A ) )
7 limord 5439 . . 3  |-  ( Lim 
A  ->  Ord  A )
8 ordtr 5394 . . 3  |-  ( Ord 
A  ->  Tr  A
)
9 trsuc 5464 . . . 4  |-  ( ( Tr  A  /\  suc  B  e.  A )  ->  B  e.  A )
109ex 435 . . 3  |-  ( Tr  A  ->  ( suc  B  e.  A  ->  B  e.  A ) )
117, 8, 103syl 18 . 2  |-  ( Lim 
A  ->  ( suc  B  e.  A  ->  B  e.  A ) )
126, 11impbid 193 1  |-  ( Lim 
A  ->  ( B  e.  A  <->  suc  B  e.  A
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ w3a 982    = wceq 1437    e. wcel 1872   A.wral 2709   (/)c0 3699   Tr wtr 4456   Ord word 5379   Lim wlim 5381   suc csuc 5382
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-sep 4484  ax-nul 4493  ax-pr 4598  ax-un 6536
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-ral 2714  df-rex 2715  df-rab 2718  df-v 3019  df-sbc 3238  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-pss 3390  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-uni 4158  df-br 4362  df-opab 4421  df-tr 4457  df-eprel 4702  df-po 4712  df-so 4713  df-fr 4750  df-we 4752  df-ord 5383  df-on 5384  df-lim 5385  df-suc 5386
This theorem is referenced by:  limsssuc  6630  limuni3  6632  peano2b  6661  rdgsucg  7091  rdgsucmptnf  7097  oesuclem  7177  oaordi  7197  omordi  7217  oeordi  7238  oelim2  7246  limenpsi  7695  r1tr  8194  r1ordg  8196  r1pwss  8202  r1val1  8204  rankdmr1  8219  rankr1bg  8221  pwwf  8225  rankr1c  8239  rankonidlem  8246  ranklim  8262  r1pwcl  8265  rankxplim3  8299  infxpenlem  8391  alephordi  8451  cflm  8626  cfslb2n  8644  alephreg  8953  r1limwun  9107  rankcf  9148  inatsk  9149
  Copyright terms: Public domain W3C validator