Theorem onsuc 7786

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

Syntax hints:   → wi 4   ∈ wcel 2107  Vcvv 3475  Oncon0 6356  suc csuc 6358

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 5295  ax-nul 5302  ax-pr 5423  ax-un 7712

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 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3965  df-nul 4321  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4905  df-br 5145  df-opab 5207  df-tr 5262  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-ord 6359  df-on 6360  df-suc 6362

This theorem is referenced by:  ordsucOLD  7789  unon  7806  onsuci  7814  ordunisuc2  7820  ordzsl  7821  onzsl  7822  tfindsg  7837  dfom2  7844  findsg  7877  tfrlem12  8376  oasuc  8511  omsuc  8513  onasuc  8515  oacl  8522  oneo  8569  omeulem1  8570  omeulem2  8571  oeordi  8575  oeworde  8581  oelim2  8583  oelimcl  8588  oeeulem  8589  oeeui  8590  oaabs2  8636  omxpenlem  9061  card2inf  9537  cantnflt  9654  cantnflem1d  9670  cnfcom  9682  r1ordg  9760  bndrank  9823  r1pw  9827  r1pwALT  9828  tcrank  9866  onssnum  10022  dfac12lem2  10126  cfsuc  10239  cfsmolem  10252  fin1a2lem1  10382  fin1a2lem2  10383  ttukeylem7  10497  alephreg  10564  gch2  10657  winainflem  10675  winalim2  10678  r1wunlim  10719  nqereu  10911  noextend  27136  noresle  27167  nosupno  27173  madeoldsuc  27346  ontgval  35221  ontgsucval  35222  onsuctop  35223  sucneqond  36151  onexgt  41860  onexomgt  41861  onexoegt  41864  onepsuc  41872  onsucelab  41884  ordnexbtwnsuc  41888  onsucrn  41892  cantnftermord  41941  cantnfub2  41943  omabs2  41953  onsucunipr  41993  onsucunitp  41994  nadd1suc  42013  naddsuc2  42014  naddwordnexlem0  42018  naddwordnexlem1  42019  minregex  42156  onsetreclem2  47591