Theorem onsuc 7765

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3442  Oncon0 6325  suc csuc 6327

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-tr 5208  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-ord 6328  df-on 6329  df-suc 6331

This theorem is referenced by:  unon  7783  onsuci  7791  ordunisuc2  7796  ordzsl  7797  onzsl  7798  tfindsg  7813  dfom2  7820  findsg  7849  tfrlem12  8330  oasuc  8461  omsuc  8463  onasuc  8465  oacl  8472  oneo  8518  omeulem1  8519  omeulem2  8520  oeordi  8525  oeworde  8531  oelim2  8533  oelimcl  8538  oeeulem  8539  oeeui  8540  oaabs2  8587  naddsuc2  8639  omxpenlem  9018  card2inf  9472  cantnflt  9593  cantnflem1d  9609  cnfcom  9621  r1ordg  9702  bndrank  9765  r1pw  9769  r1pwALT  9770  tcrank  9808  onssnum  9962  dfac12lem2  10067  cfsuc  10179  cfsmolem  10192  fin1a2lem1  10322  fin1a2lem2  10323  ttukeylem7  10437  alephreg  10505  gch2  10598  winainflem  10616  winalim2  10619  r1wunlim  10660  nqereu  10852  noextend  27646  noresle  27677  nosupno  27683  madeoldsuc  27893  bdayn0p1  28377  constrextdg2lem  33926  fineqvnttrclselem2  35300  ontgval  36647  ontgsucval  36648  onsuctop  36649  sucneqond  37620  onexgt  43597  onexomgt  43598  onexoegt  43601  onepsuc  43609  onsucelab  43620  ordnexbtwnsuc  43624  onsucrn  43628  cantnftermord  43677  cantnfub2  43679  omabs2  43689  onsucunipr  43729  onsucunitp  43730  nadd1suc  43749  naddwordnexlem0  43753  naddwordnexlem1  43754  minregex  43890  onsetreclem2  50065