Theorem onsuc 7805

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2143  Vcvv 3455  Oncon0 6360  suc csuc 6362

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404  ax-un 7732

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-tr 5219  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-ord 6363  df-on 6364  df-suc 6366

This theorem is used by:  unon  7823  onsuci  7831  ordunisuc2  7836  ordzsl  7837  onzsl  7838  tfindsg  7853  dfom2  7860  findsg  7890  tfrlem12  8372  oasuc  8505  omsuc  8507  onasuc  8509  oacl  8516  oneo  8562  omeulem1  8563  omeulem2  8564  oeordi  8569  oeworde  8575  oelim2  8577  oelimcl  8582  oeeulem  8583  oeeui  8584  oaabs2  8631  naddsuc2  8684  omxpenlem  9062  card2inf  9513  cantnflt  9637  cantnflem1d  9653  cnfcom  9665  r1ordg  9746  bndrank  9809  r1pw  9813  r1pwALT  9814  tcrank  9852  onssnum  10029  dfac12lem2  10133  cfsuc  10245  cfsmolem  10258  fin1a2lem1  10388  fin1a2lem2  10389  ttukeylem7  10503  alephreg  10571  gch2  10664  winainflem  10682  winalim2  10685  r1wunlim  10726  nqereu  10918  noextend  27839  noresle  27870  nosupno  27876  madeoldsuc  28087  bdayn0p1  28571  constrextdg2lem  34147  fineqvnttrclselem2  35543  nmulprop  36690  ontgval  36970  ontgsucval  36971  onsuctop  36972  sucneqond  38039  onexgt  43995  onexomgt  43996  onexoegt  43999  onepsuc  44007  onsucelab  44018  ordnexbtwnsuc  44022  onsucrn  44026  cantnftermord  44075  cantnfub2  44077  omabs2  44087  onsucunipr  44127  onsucunitp  44128  nadd1suc  44147  naddwordnexlem0  44151  naddwordnexlem1  44152  minregex  44288  onsetreclem2  50512