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

Theorem limsuc 4770
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 4769 . . 3  |-  ( Lim 
A  <->  ( Ord  A  /\  (/)  e.  A  /\  A. x  e.  A  suc  x  e.  A )
)
2 suceq 4588 . . . . . 6  |-  ( x  =  B  ->  suc  x  =  suc  B )
32eleq1d 2454 . . . . 5  |-  ( x  =  B  ->  ( suc  x  e.  A  <->  suc  B  e.  A ) )
43rspccv 2993 . . . 4  |-  ( A. x  e.  A  suc  x  e.  A  ->  ( B  e.  A  ->  suc  B  e.  A ) )
543ad2ant3 980 . . 3  |-  ( ( Ord  A  /\  (/)  e.  A  /\  A. x  e.  A  suc  x  e.  A )  ->  ( B  e.  A  ->  suc  B  e.  A ) )
61, 5sylbi 188 . 2  |-  ( Lim 
A  ->  ( B  e.  A  ->  suc  B  e.  A ) )
7 limord 4582 . . 3  |-  ( Lim 
A  ->  Ord  A )
8 ordtr 4537 . . 3  |-  ( Ord 
A  ->  Tr  A
)
9 trsuc 4607 . . . 4  |-  ( ( Tr  A  /\  suc  B  e.  A )  ->  B  e.  A )
109ex 424 . . 3  |-  ( Tr  A  ->  ( suc  B  e.  A  ->  B  e.  A ) )
117, 8, 103syl 19 . 2  |-  ( Lim 
A  ->  ( suc  B  e.  A  ->  B  e.  A ) )
126, 11impbid 184 1  |-  ( Lim 
A  ->  ( B  e.  A  <->  suc  B  e.  A
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ w3a 936    = wceq 1649    e. wcel 1717   A.wral 2650   (/)c0 3572   Tr wtr 4244   Ord word 4522   Lim wlim 4524   suc csuc 4525
This theorem is referenced by:  limsssuc  4771  limuni3  4773  peano2b  4802  rdgsucg  6618  rdgsucmptnf  6624  oesuclem  6706  oaordi  6726  omordi  6746  oeordi  6767  oelim2  6775  limenpsi  7219  r1tr  7636  r1ordg  7638  r1pwss  7644  r1val1  7646  rankdmr1  7661  rankr1bg  7663  pwwf  7667  rankr1c  7681  rankonidlem  7688  ranklim  7704  r1pwcl  7707  rankxplim3  7739  infxpenlem  7829  alephordi  7889  cflm  8064  cfslb2n  8082  alephreg  8391  r1limwun  8545  rankcf  8586  inatsk  8587
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 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369  ax-sep 4272  ax-nul 4280  ax-pr 4345  ax-un 4642
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 2243  df-mo 2244  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-ne 2553  df-ral 2655  df-rex 2656  df-rab 2659  df-v 2902  df-sbc 3106  df-dif 3267  df-un 3269  df-in 3271  df-ss 3278  df-pss 3280  df-nul 3573  df-if 3684  df-pw 3745  df-sn 3764  df-pr 3765  df-tp 3766  df-op 3767  df-uni 3959  df-br 4155  df-opab 4209  df-tr 4245  df-eprel 4436  df-po 4445  df-so 4446  df-fr 4483  df-we 4485  df-ord 4526  df-on 4527  df-lim 4528  df-suc 4529
  Copyright terms: Public domain W3C validator