Theorem onsuc 7808

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

Syntax hints:   → wi 4   ∈ wcel 2149  Vcvv 3463  Oncon0 6361  suc csuc 6363

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pr 5405  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-tr 5223  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-ord 6364  df-on 6365  df-suc 6367

This theorem is referenced by:  unon  7826  onsuci  7834  ordunisuc2  7839  ordzsl  7840  onzsl  7841  tfindsg  7856  dfom2  7863  findsg  7893  tfrlem12  8375  oasuc  8508  omsuc  8510  onasuc  8512  oacl  8519  oneo  8565  omeulem1  8566  omeulem2  8567  oeordi  8572  oeworde  8578  oelim2  8580  oelimcl  8585  oeeulem  8586  oeeui  8587  oaabs2  8634  naddsuc2  8687  omxpenlem  9065  card2inf  9516  cantnflt  9640  cantnflem1d  9656  cnfcom  9668  r1ordg  9749  bndrank  9812  r1pw  9816  r1pwALT  9817  tcrank  9855  onssnum  10023  dfac12lem2  10127  cfsuc  10240  cfsmolem  10253  fin1a2lem1  10383  fin1a2lem2  10384  ttukeylem7  10498  alephreg  10566  gch2  10659  winainflem  10677  winalim2  10680  r1wunlim  10721  nqereu  10913  noextend  27795  noresle  27826  nosupno  27832  madeoldsuc  28043  bdayn0p1  28527  constrextdg2lem  34082  fineqvnttrclselem2  35457  nmulprop  36580  ontgval  36830  ontgsucval  36831  onsuctop  36832  sucneqond  37898  onexgt  43858  onexomgt  43859  onexoegt  43862  onepsuc  43870  onsucelab  43881  ordnexbtwnsuc  43885  onsucrn  43889  cantnftermord  43938  cantnfub2  43940  omabs2  43950  onsucunipr  43990  onsucunitp  43991  nadd1suc  44010  naddwordnexlem0  44014  naddwordnexlem1  44015  minregex  44151  onsetreclem2  50368