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)

Syntax hints:   → wi 4   ∈ wcel 2143  Vcvv 3455  Oncon0 6360  suc csuc 6362

This theorem was proved from 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 theorem 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 referenced 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  10020  dfac12lem2  10124  cfsuc  10236  cfsmolem  10249  fin1a2lem1  10379  fin1a2lem2  10380  ttukeylem7  10494  alephreg  10562  gch2  10655  winainflem  10673  winalim2  10676  r1wunlim  10717  nqereu  10909  noextend  27830  noresle  27861  nosupno  27867  madeoldsuc  28078  bdayn0p1  28562  constrextdg2lem  34138  fineqvnttrclselem2  35535  nmulprop  36682  ontgval  36942  ontgsucval  36943  onsuctop  36944  sucneqond  38011  onexgt  43967  onexomgt  43968  onexoegt  43971  onepsuc  43979  onsucelab  43990  ordnexbtwnsuc  43994  onsucrn  43998  cantnftermord  44047  cantnfub2  44049  omabs2  44059  onsucunipr  44099  onsucunitp  44100  nadd1suc  44119  naddwordnexlem0  44123  naddwordnexlem1  44124  minregex  44260  onsetreclem2  50484