Theorem onsuc 7743

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

Syntax hints:   → wi 4   ∈ wcel 2111  Vcvv 3436  Oncon0 6306  suc csuc 6308

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-tr 5197  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-we 5569  df-ord 6309  df-on 6310  df-suc 6312

This theorem is referenced by:  unon  7761  onsuci  7769  ordunisuc2  7774  ordzsl  7775  onzsl  7776  tfindsg  7791  dfom2  7798  findsg  7827  tfrlem12  8308  oasuc  8439  omsuc  8441  onasuc  8443  oacl  8450  oneo  8496  omeulem1  8497  omeulem2  8498  oeordi  8502  oeworde  8508  oelim2  8510  oelimcl  8515  oeeulem  8516  oeeui  8517  oaabs2  8564  naddsuc2  8616  omxpenlem  8991  card2inf  9441  cantnflt  9562  cantnflem1d  9578  cnfcom  9590  r1ordg  9671  bndrank  9734  r1pw  9738  r1pwALT  9739  tcrank  9777  onssnum  9931  dfac12lem2  10036  cfsuc  10148  cfsmolem  10161  fin1a2lem1  10291  fin1a2lem2  10292  ttukeylem7  10406  alephreg  10473  gch2  10566  winainflem  10584  winalim2  10587  r1wunlim  10628  nqereu  10820  noextend  27605  noresle  27636  nosupno  27642  madeoldsuc  27830  bdayn0p1  28294  constrextdg2lem  33761  fineqvnttrclselem2  35142  ontgval  36473  ontgsucval  36474  onsuctop  36475  sucneqond  37407  onexgt  43281  onexomgt  43282  onexoegt  43285  onepsuc  43293  onsucelab  43304  ordnexbtwnsuc  43308  onsucrn  43312  cantnftermord  43361  cantnfub2  43363  omabs2  43373  onsucunipr  43413  onsucunitp  43414  nadd1suc  43433  naddwordnexlem0  43437  naddwordnexlem1  43438  minregex  43575  onsetreclem2  49746