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  27554  noresle  27585  nosupno  27591  madeoldsuc  27772  bdayn0p1  28234  constrextdg2lem  33711  ontgval  36392  ontgsucval  36393  onsuctop  36394  sucneqond  37326  onexgt  43202  onexomgt  43203  onexoegt  43206  onepsuc  43214  onsucelab  43225  ordnexbtwnsuc  43229  onsucrn  43233  cantnftermord  43282  cantnfub2  43284  omabs2  43294  onsucunipr  43334  onsucunitp  43335  nadd1suc  43354  naddwordnexlem0  43358  naddwordnexlem1  43359  minregex  43496  onsetreclem2  49668