Theorem onsuc 7767

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3444  Oncon0 6320  suc csuc 6322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382  ax-un 7691

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-tr 5210  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-ord 6323  df-on 6324  df-suc 6326

This theorem is referenced by:  ordsucOLD  7769  unon  7786  onsuci  7794  ordunisuc2  7800  ordzsl  7801  onzsl  7802  tfindsg  7817  dfom2  7824  findsg  7853  tfrlem12  8334  oasuc  8465  omsuc  8467  onasuc  8469  oacl  8476  oneo  8522  omeulem1  8523  omeulem2  8524  oeordi  8528  oeworde  8534  oelim2  8536  oelimcl  8541  oeeulem  8542  oeeui  8543  oaabs2  8590  naddsuc2  8642  omxpenlem  9019  card2inf  9484  cantnflt  9601  cantnflem1d  9617  cnfcom  9629  r1ordg  9707  bndrank  9770  r1pw  9774  r1pwALT  9775  tcrank  9813  onssnum  9969  dfac12lem2  10074  cfsuc  10186  cfsmolem  10199  fin1a2lem1  10329  fin1a2lem2  10330  ttukeylem7  10444  alephreg  10511  gch2  10604  winainflem  10622  winalim2  10625  r1wunlim  10666  nqereu  10858  noextend  27611  noresle  27642  nosupno  27648  madeoldsuc  27834  bdayn0p1  28298  constrextdg2lem  33731  ontgval  36412  ontgsucval  36413  onsuctop  36414  sucneqond  37346  onexgt  43222  onexomgt  43223  onexoegt  43226  onepsuc  43234  onsucelab  43245  ordnexbtwnsuc  43249  onsucrn  43253  cantnftermord  43302  cantnfub2  43304  omabs2  43314  onsucunipr  43354  onsucunitp  43355  nadd1suc  43374  naddwordnexlem0  43378  naddwordnexlem1  43379  minregex  43516  onsetreclem2  49688