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

Theorem limsuc 4771
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 4770 . . 3  |-  ( Lim 
A  <->  ( Ord  A  /\  (/)  e.  A  /\  A. x  e.  A  suc  x  e.  A )
)
2 suceq 4589 . . . . . 6  |-  ( x  =  B  ->  suc  x  =  suc  B )
32eleq1d 2455 . . . . 5  |-  ( x  =  B  ->  ( suc  x  e.  A  <->  suc  B  e.  A ) )
43rspccv 2994 . . . 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 4583 . . 3  |-  ( Lim 
A  ->  Ord  A )
8 ordtr 4538 . . 3  |-  ( Ord 
A  ->  Tr  A
)
9 trsuc 4608 . . . 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 2651   (/)c0 3573   Tr wtr 4245   Ord word 4523   Lim wlim 4525   suc csuc 4526
This theorem is referenced by:  limsssuc  4772  limuni3  4774  peano2b  4803  rdgsucg  6619  rdgsucmptnf  6625  oesuclem  6707  oaordi  6727  omordi  6747  oeordi  6768  oelim2  6776  limenpsi  7220  r1tr  7637  r1ordg  7639  r1pwss  7645  r1val1  7647  rankdmr1  7662  rankr1bg  7664  pwwf  7668  rankr1c  7682  rankonidlem  7689  ranklim  7705  r1pwcl  7708  rankxplim3  7740  infxpenlem  7830  alephordi  7890  cflm  8065  cfslb2n  8083  alephreg  8392  r1limwun  8546  rankcf  8587  inatsk  8588
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 2370  ax-sep 4273  ax-nul 4281  ax-pr 4346  ax-un 4643
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 2244  df-mo 2245  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ne 2554  df-ral 2656  df-rex 2657  df-rab 2660  df-v 2903  df-sbc 3107  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-pss 3281  df-nul 3574  df-if 3685  df-pw 3746  df-sn 3765  df-pr 3766  df-tp 3767  df-op 3768  df-uni 3960  df-br 4156  df-opab 4210  df-tr 4246  df-eprel 4437  df-po 4446  df-so 4447  df-fr 4484  df-we 4486  df-ord 4527  df-on 4528  df-lim 4529  df-suc 4530
  Copyright terms: Public domain W3C validator