Theorem peano2b 7577

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 7576	. 2 ⊢ Lim ω
2		limsuc 7545	. 2 ⊢ (Lim ω → (𝐴 ∈ ω ↔ suc 𝐴 ∈ ω))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ ω ↔ suc 𝐴 ∈ ω)

Syntax hints:   ↔ wb 208   ∈ wcel 2114  Lim wlim 6173  suc csuc 6174  ωcom 7561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-sep 5184  ax-nul 5191  ax-pr 5311  ax-un 7442

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3012  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3483  df-sbc 3759  df-dif 3922  df-un 3924  df-in 3926  df-ss 3935  df-pss 3937  df-nul 4275  df-if 4449  df-pw 4522  df-sn 4549  df-pr 4551  df-tp 4553  df-op 4555  df-uni 4820  df-br 5048  df-opab 5110  df-tr 5154  df-eprel 5446  df-po 5455  df-so 5456  df-fr 5495  df-we 5497  df-ord 6175  df-on 6176  df-lim 6177  df-suc 6178  df-om 7562

This theorem is referenced by:  nnsuc  7578  peano2  7583  peano5  7586  frsuc  8053  frsucmptn  8055  nnaordi  8225  nnmsucr  8232  omsmolem  8261  php  8682  php4  8685  unblem1  8751  isfinite2  8757  inf0  9065  inf3lem1  9072  inf3lem5  9076  cantnfp1lem3  9124  cantnflem1  9133  itunisuc  9822  ituniiun  9825  indpi  10310  rdgeqoa  34662