Theorem limsuc 7830

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.

Step	Hyp	Ref	Expression
1		dflim4 7829	. . 3 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴))
2		suceq 6415	. . . . . 6 ⊢ (𝑥 = 𝐵 → suc 𝑥 = suc 𝐵)
3	2	eleq1d 2848	. . . . 5 ⊢ (𝑥 = 𝐵 → (suc 𝑥 ∈ 𝐴 ↔ suc 𝐵 ∈ 𝐴))
4	3	rspccv 3579	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 → (𝐵 ∈ 𝐴 → suc 𝐵 ∈ 𝐴))
5	4	3ad2ant3 1149	. . 3 ⊢ ((Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴) → (𝐵 ∈ 𝐴 → suc 𝐵 ∈ 𝐴))
6	1, 5	sylbi 219	. 2 ⊢ (Lim 𝐴 → (𝐵 ∈ 𝐴 → suc 𝐵 ∈ 𝐴))
7		limord 6408	. . 3 ⊢ (Lim 𝐴 → Ord 𝐴)
8		ordtr 6361	. . 3 ⊢ (Ord 𝐴 → Tr 𝐴)
9		trsuc 6436	. . . 4 ⊢ ((Tr 𝐴 ∧ suc 𝐵 ∈ 𝐴) → 𝐵 ∈ 𝐴)
10	9	ex 416	. . 3 ⊢ (Tr 𝐴 → (suc 𝐵 ∈ 𝐴 → 𝐵 ∈ 𝐴))
11	7, 8, 10	3syl 18	. 2 ⊢ (Lim 𝐴 → (suc 𝐵 ∈ 𝐴 → 𝐵 ∈ 𝐴))
12	6, 11	impbid 214	1 ⊢ (Lim 𝐴 → (𝐵 ∈ 𝐴 ↔ suc 𝐵 ∈ 𝐴))

Syntax hints:   → wi 4   ↔ wb 208   ∧ w3a 1099   = wceq 1561   ∈ wcel 2143  ∀wral 3077  ∅c0 4286  Tr wtr 5208  Ord word 6346  Lim wlim 6348  suc csuc 6349

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5247  ax-nul 5257  ax-pr 5391  ax-un 7719

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3078  df-rex 3088  df-rab 3416  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5102  df-opab 5164  df-tr 5209  df-eprel 5548  df-po 5556  df-so 5557  df-fr 5601  df-we 5603  df-ord 6350  df-on 6351  df-lim 6352  df-suc 6353

This theorem is referenced by:  limsssuc  7831  limuni3  7833  peano2b  7864  rdgsucg  8395  rdgsucmptnf  8401  oesuclem  8495  oaordi  8516  omordi  8536  oeordi  8558  oelim2  8566  limenpsi  9125  r1tr  9735  r1ordg  9737  r1pwss  9743  r1val1  9745  rankdmr1  9760  rankr1bg  9762  pwwf  9766  rankr1c  9780  rankonidlem  9787  ranklim  9803  r1pwcl  9806  rankxplim3  9840  infxpenlem  9970  alephordi  10031  cflm  10207  cfslb2n  10226  alephreg  10541  r1limwun  10695  rankcf  10736  inatsk  10737  oldlim  27981  rankfilimbi  35398  r1filimi  35400  succlg  43906