Theorem onsuc 7815

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Vcvv 3457  Oncon0 6364  suc csuc 6366

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406  ax-un 7742

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-tr 5221  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-ord 6367  df-on 6368  df-suc 6370

This theorem is used by:  unon  7833  onsuci  7841  ordunisuc2  7846  ordzsl  7847  onzsl  7848  tfindsg  7863  dfom2  7870  findsg  7900  tfrlem12  8382  oasuc  8515  omsuc  8517  onasuc  8519  oacl  8526  oneo  8572  omeulem1  8573  omeulem2  8574  oeordi  8579  oeworde  8585  oelim2  8587  oelimcl  8592  oeeulem  8593  oeeui  8594  oaabs2  8641  naddsuc2  8694  omxpenlem  9073  card2inf  9524  cantnflt  9648  cantnflem1d  9664  cnfcom  9676  r1ordg  9757  bndrank  9820  r1pw  9824  r1pwALT  9825  tcrank  9863  onssnum  10040  dfac12lem2  10144  cfsuc  10256  cfsmolem  10269  fin1a2lem1  10399  fin1a2lem2  10400  ttukeylem7  10514  alephreg  10582  gch2  10675  winainflem  10693  winalim2  10696  r1wunlim  10737  nqereu  10929  noextend  27881  noresle  27912  nosupno  27918  madeoldsuc  28129  bdayn0p1  28613  constrextdg2lem  34202  fineqvnttrclselem2  35592  nmulprop  36719  ontgval  36999  ontgsucval  37000  onsuctop  37001  sucneqond  38068  onexgt  44025  onexomgt  44026  onexoegt  44029  onepsuc  44037  onsucelab  44048  ordnexbtwnsuc  44052  onsucrn  44056  cantnftermord  44105  cantnfub2  44107  omabs2  44117  onsucunipr  44157  onsucunitp  44158  nadd1suc  44177  naddwordnexlem0  44181  naddwordnexlem1  44182  minregex  44318  onsetreclem2  50541