Theorem onsuc 7803

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

Syntax hints:   → wi 4   ∈ wcel 2105  Vcvv 3473  Oncon0 6364  suc csuc 6366

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7729

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-tr 5266  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-ord 6367  df-on 6368  df-suc 6370

This theorem is referenced by:  ordsucOLD  7806  unon  7823  onsuci  7831  ordunisuc2  7837  ordzsl  7838  onzsl  7839  tfindsg  7854  dfom2  7861  findsg  7894  tfrlem12  8395  oasuc  8530  omsuc  8532  onasuc  8534  oacl  8541  oneo  8587  omeulem1  8588  omeulem2  8589  oeordi  8593  oeworde  8599  oelim2  8601  oelimcl  8606  oeeulem  8607  oeeui  8608  oaabs2  8654  omxpenlem  9079  card2inf  9556  cantnflt  9673  cantnflem1d  9689  cnfcom  9701  r1ordg  9779  bndrank  9842  r1pw  9846  r1pwALT  9847  tcrank  9885  onssnum  10041  dfac12lem2  10145  cfsuc  10258  cfsmolem  10271  fin1a2lem1  10401  fin1a2lem2  10402  ttukeylem7  10516  alephreg  10583  gch2  10676  winainflem  10694  winalim2  10697  r1wunlim  10738  nqereu  10930  noextend  27512  noresle  27543  nosupno  27549  madeoldsuc  27724  ontgval  35780  ontgsucval  35781  onsuctop  35782  sucneqond  36710  onexgt  42452  onexomgt  42453  onexoegt  42456  onepsuc  42464  onsucelab  42476  ordnexbtwnsuc  42480  onsucrn  42484  cantnftermord  42533  cantnfub2  42535  omabs2  42545  onsucunipr  42585  onsucunitp  42586  nadd1suc  42605  naddsuc2  42606  naddwordnexlem0  42610  naddwordnexlem1  42611  minregex  42748  onsetreclem2  47913