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

Theorem limsuc 7870
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 𝐴 → (𝐵𝐴 ↔ suc 𝐵𝐴))

Proof of Theorem limsuc
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 dflim4 7869 . . 3 (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ ∀𝑥𝐴 suc 𝑥𝐴))
2 suceq 6452 . . . . . 6 (𝑥 = 𝐵 → suc 𝑥 = suc 𝐵)
32eleq1d 2824 . . . . 5 (𝑥 = 𝐵 → (suc 𝑥𝐴 ↔ suc 𝐵𝐴))
43rspccv 3619 . . . 4 (∀𝑥𝐴 suc 𝑥𝐴 → (𝐵𝐴 → suc 𝐵𝐴))
543ad2ant3 1134 . . 3 ((Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ ∀𝑥𝐴 suc 𝑥𝐴) → (𝐵𝐴 → suc 𝐵𝐴))
61, 5sylbi 217 . 2 (Lim 𝐴 → (𝐵𝐴 → suc 𝐵𝐴))
7 limord 6446 . . 3 (Lim 𝐴 → Ord 𝐴)
8 ordtr 6400 . . 3 (Ord 𝐴 → Tr 𝐴)
9 trsuc 6473 . . . 4 ((Tr 𝐴 ∧ suc 𝐵𝐴) → 𝐵𝐴)
109ex 412 . . 3 (Tr 𝐴 → (suc 𝐵𝐴𝐵𝐴))
117, 8, 103syl 18 . 2 (Lim 𝐴 → (suc 𝐵𝐴𝐵𝐴))
126, 11impbid 212 1 (Lim 𝐴 → (𝐵𝐴 ↔ suc 𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  w3a 1086   = wceq 1537  wcel 2106  wral 3059  c0 4339  Tr wtr 5265  Ord word 6385  Lim wlim 6387  suc csuc 6388
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-tr 5266  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392
This theorem is referenced by:  limsssuc  7871  limuni3  7873  peano2b  7904  rdgsucg  8462  rdgsucmptnf  8468  oesuclem  8562  oaordi  8583  omordi  8603  oeordi  8624  oelim2  8632  limenpsi  9191  r1tr  9814  r1ordg  9816  r1pwss  9822  r1val1  9824  rankdmr1  9839  rankr1bg  9841  pwwf  9845  rankr1c  9859  rankonidlem  9866  ranklim  9882  r1pwcl  9885  rankxplim3  9919  infxpenlem  10051  alephordi  10112  cflm  10288  cfslb2n  10306  alephreg  10620  r1limwun  10774  rankcf  10815  inatsk  10816  oldlim  27940  succlg  43318
  Copyright terms: Public domain W3C validator