Theorem onsuc 7753

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

Syntax hints:   → wi 4   ∈ wcel 2119  Vcvv 3431  Oncon0 6310  suc csuc 6312

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-tr 5180  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-ord 6313  df-on 6314  df-suc 6316

This theorem is referenced by:  unon  7771  onsuci  7779  ordunisuc2  7784  ordzsl  7785  onzsl  7786  tfindsg  7801  dfom2  7808  findsg  7837  tfrlem12  8318  oasuc  8449  omsuc  8451  onasuc  8453  oacl  8460  oneo  8506  omeulem1  8507  omeulem2  8508  oeordi  8513  oeworde  8519  oelim2  8521  oelimcl  8526  oeeulem  8527  oeeui  8528  oaabs2  8575  naddsuc2  8627  omxpenlem  9006  card2inf  9460  cantnflt  9584  cantnflem1d  9600  cnfcom  9612  r1ordg  9693  bndrank  9756  r1pw  9760  r1pwALT  9761  tcrank  9799  onssnum  9953  dfac12lem2  10058  cfsuc  10170  cfsmolem  10183  fin1a2lem1  10313  fin1a2lem2  10314  ttukeylem7  10428  alephreg  10496  gch2  10589  winainflem  10607  winalim2  10610  r1wunlim  10651  nqereu  10843  noextend  27648  noresle  27679  nosupno  27685  madeoldsuc  27895  bdayn0p1  28379  constrextdg2lem  33932  fineqvnttrclselem2  35303  ontgval  36659  ontgsucval  36660  onsuctop  36661  sucneqond  37727  onexgt  43685  onexomgt  43686  onexoegt  43689  onepsuc  43697  onsucelab  43708  ordnexbtwnsuc  43712  onsucrn  43716  cantnftermord  43765  cantnfub2  43767  omabs2  43777  onsucunipr  43817  onsucunitp  43818  nadd1suc  43837  naddwordnexlem0  43841  naddwordnexlem1  43842  minregex  43978  onsetreclem2  50196