Theorem limsuc 7803

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 7802	. . 3 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴))
2		suceq 6395	. . . . . 6 ⊢ (𝑥 = 𝐵 → suc 𝑥 = suc 𝐵)
3	2	eleq1d 2822	. . . . 5 ⊢ (𝑥 = 𝐵 → (suc 𝑥 ∈ 𝐴 ↔ suc 𝐵 ∈ 𝐴))
4	3	rspccv 3575	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 → (𝐵 ∈ 𝐴 → suc 𝐵 ∈ 𝐴))
5	4	3ad2ant3 1136	. . 3 ⊢ ((Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴) → (𝐵 ∈ 𝐴 → suc 𝐵 ∈ 𝐴))
6	1, 5	sylbi 217	. 2 ⊢ (Lim 𝐴 → (𝐵 ∈ 𝐴 → suc 𝐵 ∈ 𝐴))
7		limord 6388	. . 3 ⊢ (Lim 𝐴 → Ord 𝐴)
8		ordtr 6341	. . 3 ⊢ (Ord 𝐴 → Tr 𝐴)
9		trsuc 6416	. . . 4 ⊢ ((Tr 𝐴 ∧ suc 𝐵 ∈ 𝐴) → 𝐵 ∈ 𝐴)
10	9	ex 412	. . 3 ⊢ (Tr 𝐴 → (suc 𝐵 ∈ 𝐴 → 𝐵 ∈ 𝐴))
11	7, 8, 10	3syl 18	. 2 ⊢ (Lim 𝐴 → (suc 𝐵 ∈ 𝐴 → 𝐵 ∈ 𝐴))
12	6, 11	impbid 212	1 ⊢ (Lim 𝐴 → (𝐵 ∈ 𝐴 ↔ suc 𝐵 ∈ 𝐴))

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ∅c0 4287  Tr wtr 5207  Ord word 6326  Lim wlim 6328  suc csuc 6329

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5245  ax-nul 5255  ax-pr 5381  ax-un 7692

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-tr 5208  df-eprel 5534  df-po 5542  df-so 5543  df-fr 5587  df-we 5589  df-ord 6330  df-on 6331  df-lim 6332  df-suc 6333

This theorem is referenced by:  limsssuc  7804  limuni3  7806  peano2b  7837  rdgsucg  8366  rdgsucmptnf  8372  oesuclem  8464  oaordi  8485  omordi  8505  oeordi  8527  oelim2  8535  limenpsi  9094  r1tr  9702  r1ordg  9704  r1pwss  9710  r1val1  9712  rankdmr1  9727  rankr1bg  9729  pwwf  9733  rankr1c  9747  rankonidlem  9754  ranklim  9770  r1pwcl  9773  rankxplim3  9807  infxpenlem  9937  alephordi  9998  cflm  10174  cfslb2n  10192  alephreg  10507  r1limwun  10661  rankcf  10702  inatsk  10703  oldlim  27900  rankfilimbi  35284  r1filimi  35286  succlg  43714