Theorem onsuc 7831

Description: The successor of an ordinal number is an ordinal number. Closed form of onsuci 7859. Forward implication of onsucb 7837. 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 7825	. 2 ⊢ (𝐴 ∈ On → suc 𝐴 ∈ V)
2		sucexeloni 7829	. 2 ⊢ ((𝐴 ∈ On ∧ suc 𝐴 ∈ V) → suc 𝐴 ∈ On)
3	1, 2	mpdan 687	1 ⊢ (𝐴 ∈ On → suc 𝐴 ∈ On)

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3478  Oncon0 6386  suc csuc 6388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-tr 5266  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-ord 6389  df-on 6390  df-suc 6392

This theorem is referenced by:  ordsucOLD  7834  unon  7851  onsuci  7859  ordunisuc2  7865  ordzsl  7866  onzsl  7867  tfindsg  7882  dfom2  7889  findsg  7920  tfrlem12  8428  oasuc  8561  omsuc  8563  onasuc  8565  oacl  8572  oneo  8618  omeulem1  8619  omeulem2  8620  oeordi  8624  oeworde  8630  oelim2  8632  oelimcl  8637  oeeulem  8638  oeeui  8639  oaabs2  8686  naddsuc2  8738  omxpenlem  9112  card2inf  9593  cantnflt  9710  cantnflem1d  9726  cnfcom  9738  r1ordg  9816  bndrank  9879  r1pw  9883  r1pwALT  9884  tcrank  9922  onssnum  10078  dfac12lem2  10183  cfsuc  10295  cfsmolem  10308  fin1a2lem1  10438  fin1a2lem2  10439  ttukeylem7  10553  alephreg  10620  gch2  10713  winainflem  10731  winalim2  10734  r1wunlim  10775  nqereu  10967  noextend  27726  noresle  27757  nosupno  27763  madeoldsuc  27938  ontgval  36414  ontgsucval  36415  onsuctop  36416  sucneqond  37348  onexgt  43229  onexomgt  43230  onexoegt  43233  onepsuc  43241  onsucelab  43253  ordnexbtwnsuc  43257  onsucrn  43261  cantnftermord  43310  cantnfub2  43312  omabs2  43322  onsucunipr  43362  onsucunitp  43363  nadd1suc  43382  naddwordnexlem0  43386  naddwordnexlem1  43387  minregex  43524  onsetreclem2  48937