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.

Step	Hyp	Ref	Expression
1		dflim4 7869	. . 3 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴))
2		suceq 6438	. . . . . 6 ⊢ (𝑥 = 𝐵 → suc 𝑥 = suc 𝐵)
3	2	eleq1d 2849	. . . . 5 ⊢ (𝑥 = 𝐵 → (suc 𝑥 ∈ 𝐴 ↔ suc 𝐵 ∈ 𝐴))
4	3	rspccv 3577	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 → (𝐵 ∈ 𝐴 → suc 𝐵 ∈ 𝐴))
5	4	3ad2ant3 1153	. . 3 ⊢ ((Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴) → (𝐵 ∈ 𝐴 → suc 𝐵 ∈ 𝐴))
6	1, 5	sylbi 220	. 2 ⊢ (Lim 𝐴 → (𝐵 ∈ 𝐴 → suc 𝐵 ∈ 𝐴))
7		limord 6431	. . 3 ⊢ (Lim 𝐴 → Ord 𝐴)
8		ordtr 6383	. . 3 ⊢ (Ord 𝐴 → Tr 𝐴)
9		trsuc 6459	. . . 4 ⊢ ((Tr 𝐴 ∧ suc 𝐵 ∈ 𝐴) → 𝐵 ∈ 𝐴)
10	9	ex 418	. . 3 ⊢ (Tr 𝐴 → (suc 𝐵 ∈ 𝐴 → 𝐵 ∈ 𝐴))
11	7, 8, 10	3syl 19	. 2 ⊢ (Lim 𝐴 → (suc 𝐵 ∈ 𝐴 → 𝐵 ∈ 𝐴))
12	6, 11	impbid 215	1 ⊢ (Lim 𝐴 → (𝐵 ∈ 𝐴 ↔ suc 𝐵 ∈ 𝐴))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103   = wceq 1569   ∈ wcel 2146  ∀wral 3080  ∅c0 4281  Tr wtr 5215  Ord word 6368  Lim wlim 6370  suc csuc 6371

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395  ax-un 7761

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-tr 5216  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375

This theorem is used by:  limsssuc  7871  limuni3  7873  peano2b  7904  rdgsucg  8445  rdgsucmptnf  8451  oesuclem  8547  oaordi  8568  omordi  8588  oeordi  8610  oelim2  8618  limenpsi  9185  r1tr  9796  r1ordg  9798  r1pwss  9804  r1val1  9806  rankdmr1  9822  rankr1bg  9824  pwwf  9828  rankr1c  9843  rankonidlem  9851  ranklim  9871  r1pwcl  9874  rankxplim3  9911  rankfilimbi  9915  r1filimi  9916  infxpenlem  10105  alephordi  10166  cflm  10340  cfslb2n  10359  alephreg  10680  r1limwun  10834  rankcf  10875  inatsk  10876  oldlim  28288  j0ltaleph  35965  succlg  44473