Theorem onsuc 7831

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3480  Oncon0 6384  suc csuc 6386

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-tr 5260  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-ord 6387  df-on 6388  df-suc 6390

This theorem is referenced by:  ordsucOLD  7834  unon  7851  onsuci  7859  ordunisuc2  7865  ordzsl  7866  onzsl  7867  tfindsg  7882  dfom2  7889  findsg  7919  tfrlem12  8429  oasuc  8562  omsuc  8564  onasuc  8566  oacl  8573  oneo  8619  omeulem1  8620  omeulem2  8621  oeordi  8625  oeworde  8631  oelim2  8633  oelimcl  8638  oeeulem  8639  oeeui  8640  oaabs2  8687  naddsuc2  8739  omxpenlem  9113  card2inf  9595  cantnflt  9712  cantnflem1d  9728  cnfcom  9740  r1ordg  9818  bndrank  9881  r1pw  9885  r1pwALT  9886  tcrank  9924  onssnum  10080  dfac12lem2  10185  cfsuc  10297  cfsmolem  10310  fin1a2lem1  10440  fin1a2lem2  10441  ttukeylem7  10555  alephreg  10622  gch2  10715  winainflem  10733  winalim2  10736  r1wunlim  10777  nqereu  10969  noextend  27711  noresle  27742  nosupno  27748  madeoldsuc  27923  constrextdg2lem  33789  ontgval  36432  ontgsucval  36433  onsuctop  36434  sucneqond  37366  onexgt  43252  onexomgt  43253  onexoegt  43256  onepsuc  43264  onsucelab  43276  ordnexbtwnsuc  43280  onsucrn  43284  cantnftermord  43333  cantnfub2  43335  omabs2  43345  onsucunipr  43385  onsucunitp  43386  nadd1suc  43405  naddwordnexlem0  43409  naddwordnexlem1  43410  minregex  43547  onsetreclem2  49225