Theorem peano2b 7928

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2147  Lim wlim 6389  suc csuc 6390  ωcom 7911

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398  ax-un 7783

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 2102  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 4841  df-uni 4873  df-br 5109  df-opab 5174  df-tr 5219  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-om 7912

This theorem is used by:  nnsuc  7929  peano2  7935  peano5  7939  frsuc  8483  frsucmptn  8485  nnaordi  8665  nnmsucr  8672  omsmolem  8704  php  9260  php4  9263  unblem1  9322  isfinite2  9328  inf0  9659  inf3lem1  9666  inf3lem5  9670  cantnfp1lem3  9718  cantnflem1  9727  itunisuc  10536  ituniiun  10539  indpi  11031  constrllcllem  34495  constrlccllem  34496  constrcccllem  34497  mh-inf3f1  37544  rdgeqoa  38561