Theorem peano2b 7892

Description: A class belongs to omega iff its successor does. (Contributed by NM, 3-Dec-1995.)

Assertion

Ref	Expression
peano2b	⊢ (𝐴 ∈ ω ↔ suc 𝐴 ∈ ω)

Proof of Theorem peano2b

Step	Hyp	Ref	Expression
1		limom 7891	. 2 ⊢ Lim ω
2		limsuc 7858	. 2 ⊢ (Lim ω → (𝐴 ∈ ω ↔ suc 𝐴 ∈ ω))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ ω ↔ suc 𝐴 ∈ ω)

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2145  Lim wlim 6362  suc csuc 6363  ωcom 7875

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7749

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-tr 5213  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-om 7876

This theorem is used by:  nnsuc  7893  peano2  7899  peano5  7903  frsuc  8438  frsucmptn  8440  nnaordi  8620  nnmsucr  8627  omsmolem  8659  php  9215  php4  9218  unblem1  9277  isfinite2  9283  inf0  9615  inf3lem1  9622  inf3lem5  9626  cantnfp1lem3  9674  cantnflem1  9683  itunisuc  10490  ituniiun  10493  indpi  10985  constrllcllem  34377  constrlccllem  34378  constrcccllem  34379  mh-inf3f1  37309  rdgeqoa  38273