Theorem onsuc 7810

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3464  Oncon0 6357  suc csuc 6359

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 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407  ax-un 7734

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 2715  df-cleq 2728  df-clel 2810  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-tr 5235  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-ord 6360  df-on 6361  df-suc 6363

This theorem is referenced by:  ordsucOLD  7813  unon  7830  onsuci  7838  ordunisuc2  7844  ordzsl  7845  onzsl  7846  tfindsg  7861  dfom2  7868  findsg  7898  tfrlem12  8408  oasuc  8541  omsuc  8543  onasuc  8545  oacl  8552  oneo  8598  omeulem1  8599  omeulem2  8600  oeordi  8604  oeworde  8610  oelim2  8612  oelimcl  8617  oeeulem  8618  oeeui  8619  oaabs2  8666  naddsuc2  8718  omxpenlem  9092  card2inf  9574  cantnflt  9691  cantnflem1d  9707  cnfcom  9719  r1ordg  9797  bndrank  9860  r1pw  9864  r1pwALT  9865  tcrank  9903  onssnum  10059  dfac12lem2  10164  cfsuc  10276  cfsmolem  10289  fin1a2lem1  10419  fin1a2lem2  10420  ttukeylem7  10534  alephreg  10601  gch2  10694  winainflem  10712  winalim2  10715  r1wunlim  10756  nqereu  10948  noextend  27635  noresle  27666  nosupno  27672  madeoldsuc  27853  bdayn0p1  28315  constrextdg2lem  33787  ontgval  36454  ontgsucval  36455  onsuctop  36456  sucneqond  37388  onexgt  43231  onexomgt  43232  onexoegt  43235  onepsuc  43243  onsucelab  43254  ordnexbtwnsuc  43258  onsucrn  43262  cantnftermord  43311  cantnfub2  43313  omabs2  43323  onsucunipr  43363  onsucunitp  43364  nadd1suc  43383  naddwordnexlem0  43387  naddwordnexlem1  43388  minregex  43525  onsetreclem2  49537