Theorem onsuc 7787

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 7781	. 2 ⊢ (𝐴 ∈ On → suc 𝐴 ∈ V)
2		sucexeloni 7785	. 2 ⊢ ((𝐴 ∈ On ∧ suc 𝐴 ∈ V) → suc 𝐴 ∈ On)
3	1, 2	mpdan 687	1 ⊢ (𝐴 ∈ On → suc 𝐴 ∈ On)

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3447  Oncon0 6332  suc csuc 6334

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-tr 5215  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-ord 6335  df-on 6336  df-suc 6338

This theorem is referenced by:  ordsucOLD  7789  unon  7806  onsuci  7814  ordunisuc2  7820  ordzsl  7821  onzsl  7822  tfindsg  7837  dfom2  7844  findsg  7873  tfrlem12  8357  oasuc  8488  omsuc  8490  onasuc  8492  oacl  8499  oneo  8545  omeulem1  8546  omeulem2  8547  oeordi  8551  oeworde  8557  oelim2  8559  oelimcl  8564  oeeulem  8565  oeeui  8566  oaabs2  8613  naddsuc2  8665  omxpenlem  9042  card2inf  9508  cantnflt  9625  cantnflem1d  9641  cnfcom  9653  r1ordg  9731  bndrank  9794  r1pw  9798  r1pwALT  9799  tcrank  9837  onssnum  9993  dfac12lem2  10098  cfsuc  10210  cfsmolem  10223  fin1a2lem1  10353  fin1a2lem2  10354  ttukeylem7  10468  alephreg  10535  gch2  10628  winainflem  10646  winalim2  10649  r1wunlim  10690  nqereu  10882  noextend  27578  noresle  27609  nosupno  27615  madeoldsuc  27796  bdayn0p1  28258  constrextdg2lem  33738  ontgval  36419  ontgsucval  36420  onsuctop  36421  sucneqond  37353  onexgt  43229  onexomgt  43230  onexoegt  43233  onepsuc  43241  onsucelab  43252  ordnexbtwnsuc  43256  onsucrn  43260  cantnftermord  43309  cantnfub2  43311  omabs2  43321  onsucunipr  43361  onsucunitp  43362  nadd1suc  43381  naddwordnexlem0  43385  naddwordnexlem1  43386  minregex  43523  onsetreclem2  49695