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

Theorem limsuc 7595
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 7594 . . 3 (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ ∀𝑥𝐴 suc 𝑥𝐴))
2 suceq 6247 . . . . . 6 (𝑥 = 𝐵 → suc 𝑥 = suc 𝐵)
32eleq1d 2818 . . . . 5 (𝑥 = 𝐵 → (suc 𝑥𝐴 ↔ suc 𝐵𝐴))
43rspccv 3526 . . . 4 (∀𝑥𝐴 suc 𝑥𝐴 → (𝐵𝐴 → suc 𝐵𝐴))
543ad2ant3 1136 . . 3 ((Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ ∀𝑥𝐴 suc 𝑥𝐴) → (𝐵𝐴 → suc 𝐵𝐴))
61, 5sylbi 220 . 2 (Lim 𝐴 → (𝐵𝐴 → suc 𝐵𝐴))
7 limord 6241 . . 3 (Lim 𝐴 → Ord 𝐴)
8 ordtr 6196 . . 3 (Ord 𝐴 → Tr 𝐴)
9 trsuc 6266 . . . 4 ((Tr 𝐴 ∧ suc 𝐵𝐴) → 𝐵𝐴)
109ex 416 . . 3 (Tr 𝐴 → (suc 𝐵𝐴𝐵𝐴))
117, 8, 103syl 18 . 2 (Lim 𝐴 → (suc 𝐵𝐴𝐵𝐴))
126, 11impbid 215 1 (Lim 𝐴 → (𝐵𝐴 ↔ suc 𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  w3a 1088   = wceq 1542  wcel 2114  wral 3054  c0 4221  Tr wtr 5146  Ord word 6181  Lim wlim 6183  suc csuc 6184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-11 2162  ax-ext 2711  ax-sep 5177  ax-nul 5184  ax-pr 5306  ax-un 7491
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-ne 2936  df-ral 3059  df-rex 3060  df-rab 3063  df-v 3402  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-pss 3872  df-nul 4222  df-if 4425  df-pw 4500  df-sn 4527  df-pr 4529  df-tp 4531  df-op 4533  df-uni 4807  df-br 5041  df-opab 5103  df-tr 5147  df-eprel 5444  df-po 5452  df-so 5453  df-fr 5493  df-we 5495  df-ord 6185  df-on 6186  df-lim 6187  df-suc 6188
This theorem is referenced by:  limsssuc  7596  limuni3  7598  peano2b  7627  rdgsucg  8100  rdgsucmptnf  8106  oesuclem  8193  oaordi  8215  omordi  8235  oeordi  8256  oelim2  8264  limenpsi  8754  r1tr  9290  r1ordg  9292  r1pwss  9298  r1val1  9300  rankdmr1  9315  rankr1bg  9317  pwwf  9321  rankr1c  9335  rankonidlem  9342  ranklim  9358  r1pwcl  9361  rankxplim3  9395  infxpenlem  9525  alephordi  9586  cflm  9762  cfslb2n  9780  alephreg  10094  r1limwun  10248  rankcf  10289  inatsk  10290  oldlim  33724
  Copyright terms: Public domain W3C validator