Theorem onsuc 7847

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3488  Oncon0 6395  suc csuc 6397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-tr 5284  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-ord 6398  df-on 6399  df-suc 6401

This theorem is referenced by:  ordsucOLD  7850  unon  7867  onsuci  7875  ordunisuc2  7881  ordzsl  7882  onzsl  7883  tfindsg  7898  dfom2  7905  findsg  7937  tfrlem12  8445  oasuc  8580  omsuc  8582  onasuc  8584  oacl  8591  oneo  8637  omeulem1  8638  omeulem2  8639  oeordi  8643  oeworde  8649  oelim2  8651  oelimcl  8656  oeeulem  8657  oeeui  8658  oaabs2  8705  naddsuc2  8757  omxpenlem  9139  card2inf  9624  cantnflt  9741  cantnflem1d  9757  cnfcom  9769  r1ordg  9847  bndrank  9910  r1pw  9914  r1pwALT  9915  tcrank  9953  onssnum  10109  dfac12lem2  10214  cfsuc  10326  cfsmolem  10339  fin1a2lem1  10469  fin1a2lem2  10470  ttukeylem7  10584  alephreg  10651  gch2  10744  winainflem  10762  winalim2  10765  r1wunlim  10806  nqereu  10998  noextend  27729  noresle  27760  nosupno  27766  madeoldsuc  27941  ontgval  36397  ontgsucval  36398  onsuctop  36399  sucneqond  37331  onexgt  43201  onexomgt  43202  onexoegt  43205  onepsuc  43213  onsucelab  43225  ordnexbtwnsuc  43229  onsucrn  43233  cantnftermord  43282  cantnfub2  43284  omabs2  43294  onsucunipr  43334  onsucunitp  43335  nadd1suc  43354  naddwordnexlem0  43358  naddwordnexlem1  43359  minregex  43496  onsetreclem2  48798