Theorem onsuc 7790

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3450  Oncon0 6335  suc csuc 6337

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714

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 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-tr 5218  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-ord 6338  df-on 6339  df-suc 6341

This theorem is referenced by:  ordsucOLD  7792  unon  7809  onsuci  7817  ordunisuc2  7823  ordzsl  7824  onzsl  7825  tfindsg  7840  dfom2  7847  findsg  7876  tfrlem12  8360  oasuc  8491  omsuc  8493  onasuc  8495  oacl  8502  oneo  8548  omeulem1  8549  omeulem2  8550  oeordi  8554  oeworde  8560  oelim2  8562  oelimcl  8567  oeeulem  8568  oeeui  8569  oaabs2  8616  naddsuc2  8668  omxpenlem  9047  card2inf  9515  cantnflt  9632  cantnflem1d  9648  cnfcom  9660  r1ordg  9738  bndrank  9801  r1pw  9805  r1pwALT  9806  tcrank  9844  onssnum  10000  dfac12lem2  10105  cfsuc  10217  cfsmolem  10230  fin1a2lem1  10360  fin1a2lem2  10361  ttukeylem7  10475  alephreg  10542  gch2  10635  winainflem  10653  winalim2  10656  r1wunlim  10697  nqereu  10889  noextend  27585  noresle  27616  nosupno  27622  madeoldsuc  27803  bdayn0p1  28265  constrextdg2lem  33745  ontgval  36426  ontgsucval  36427  onsuctop  36428  sucneqond  37360  onexgt  43236  onexomgt  43237  onexoegt  43240  onepsuc  43248  onsucelab  43259  ordnexbtwnsuc  43263  onsucrn  43267  cantnftermord  43316  cantnfub2  43318  omabs2  43328  onsucunipr  43368  onsucunitp  43369  nadd1suc  43388  naddwordnexlem0  43392  naddwordnexlem1  43393  minregex  43530  onsetreclem2  49699