Theorem onsuc 7794

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

Syntax hints:   → wi 4   ∈ wcel 2107  Vcvv 3475  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 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7720

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-tr 5265  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-ord 6364  df-on 6365  df-suc 6367

This theorem is referenced by:  ordsucOLD  7797  unon  7814  onsuci  7822  ordunisuc2  7828  ordzsl  7829  onzsl  7830  tfindsg  7845  dfom2  7852  findsg  7885  tfrlem12  8384  oasuc  8519  omsuc  8521  onasuc  8523  oacl  8530  oneo  8577  omeulem1  8578  omeulem2  8579  oeordi  8583  oeworde  8589  oelim2  8591  oelimcl  8596  oeeulem  8597  oeeui  8598  oaabs2  8644  omxpenlem  9069  card2inf  9546  cantnflt  9663  cantnflem1d  9679  cnfcom  9691  r1ordg  9769  bndrank  9832  r1pw  9836  r1pwALT  9837  tcrank  9875  onssnum  10031  dfac12lem2  10135  cfsuc  10248  cfsmolem  10261  fin1a2lem1  10391  fin1a2lem2  10392  ttukeylem7  10506  alephreg  10573  gch2  10666  winainflem  10684  winalim2  10687  r1wunlim  10728  nqereu  10920  noextend  27149  noresle  27180  nosupno  27186  madeoldsuc  27359  ontgval  35254  ontgsucval  35255  onsuctop  35256  sucneqond  36184  onexgt  41922  onexomgt  41923  onexoegt  41926  onepsuc  41934  onsucelab  41946  ordnexbtwnsuc  41950  onsucrn  41954  cantnftermord  42003  cantnfub2  42005  omabs2  42015  onsucunipr  42055  onsucunitp  42056  nadd1suc  42075  naddsuc2  42076  naddwordnexlem0  42080  naddwordnexlem1  42081  minregex  42218  onsetreclem2  47653