Theorem onsuc 7757

Description: The successor of an ordinal number is an ordinal number. Closed form of onsuci 7783. Forward implication of onsucb 7761. Proposition 7.24 of [TakeutiZaring] p. 41. Remark 1.5 of [Schloeder] p. 1. (Contributed by NM, 6-Jun-1994.) (Proof shortened by BTernaryTau, 30-Nov-2024.)

Assertion

Ref	Expression
onsuc	⊢ (𝐴 ∈ On → suc 𝐴 ∈ On)

Proof of Theorem onsuc

Step	Hyp	Ref	Expression
1		sucexg 7752	. 2 ⊢ (𝐴 ∈ On → suc 𝐴 ∈ V)
2		sucexeloni 7756	. 2 ⊢ ((𝐴 ∈ On ∧ suc 𝐴 ∈ V) → suc 𝐴 ∈ On)
3	1, 2	mpdan 688	1 ⊢ (𝐴 ∈ On → suc 𝐴 ∈ On)

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3441  Oncon0 6318  suc csuc 6320

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 5242  ax-nul 5252  ax-pr 5378  ax-un 7682

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 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-tr 5207  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-ord 6321  df-on 6322  df-suc 6324

This theorem is referenced by:  unon  7775  onsuci  7783  ordunisuc2  7788  ordzsl  7789  onzsl  7790  tfindsg  7805  dfom2  7812  findsg  7841  tfrlem12  8322  oasuc  8453  omsuc  8455  onasuc  8457  oacl  8464  oneo  8510  omeulem1  8511  omeulem2  8512  oeordi  8517  oeworde  8523  oelim2  8525  oelimcl  8530  oeeulem  8531  oeeui  8532  oaabs2  8579  naddsuc2  8631  omxpenlem  9010  card2inf  9464  cantnflt  9585  cantnflem1d  9601  cnfcom  9613  r1ordg  9694  bndrank  9757  r1pw  9761  r1pwALT  9762  tcrank  9800  onssnum  9954  dfac12lem2  10059  cfsuc  10171  cfsmolem  10184  fin1a2lem1  10314  fin1a2lem2  10315  ttukeylem7  10429  alephreg  10497  gch2  10590  winainflem  10608  winalim2  10611  r1wunlim  10652  nqereu  10844  noextend  27638  noresle  27669  nosupno  27675  madeoldsuc  27867  bdayn0p1  28348  constrextdg2lem  33886  fineqvnttrclselem2  35259  ontgval  36606  ontgsucval  36607  onsuctop  36608  sucneqond  37541  onexgt  43518  onexomgt  43519  onexoegt  43522  onepsuc  43530  onsucelab  43541  ordnexbtwnsuc  43545  onsucrn  43549  cantnftermord  43598  cantnfub2  43600  omabs2  43610  onsucunipr  43650  onsucunitp  43651  nadd1suc  43670  naddwordnexlem0  43674  naddwordnexlem1  43675  minregex  43811  onsetreclem2  49987