Theorem onsuc 7828

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Vcvv 3450  Oncon0 6365  suc csuc 6367

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5391  ax-un 7755

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-tr 5212  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6368  df-on 6369  df-suc 6371

This theorem is used by:  unon  7846  onsuci  7854  ordunisuc2  7859  ordzsl  7860  onzsl  7861  tfindsg  7876  dfom2  7883  findsg  7913  tfrlem12  8404  oasuc  8539  omsuc  8541  onasuc  8543  oacl  8550  oneo  8596  omeulem1  8597  omeulem2  8598  oeordi  8603  oeworde  8609  oelim2  8611  oelimcl  8616  oeeulem  8617  oeeui  8618  oaabs2  8665  naddsuc2  8718  omxpenlem  9104  card2inf  9556  cantnflt  9680  cantnflem1d  9696  cnfcom  9708  r1ordg  9792  bndrank  9861  r1pw  9866  r1pwALT  9867  tcrank  9908  onssnum  10126  dfac12lem2  10230  cfsuc  10342  cfsmolem  10355  fin1a2lem1  10485  fin1a2lem2  10486  ttukeylem7  10600  alephreg  10674  gch2  10767  winainflem  10785  winalim2  10788  r1wunlim  10829  nqereu  11021  noextend  28032  noresle  28063  nosupno  28069  madeoldsuc  28280  bdayn0p1  28764  constrextdg2lem  34430  fineqvnttrclselem2  35850  j0ltalephlem  35950  j0ltaleph  35951  nmulprop  37035  ontgval  37315  ontgsucval  37316  onsuctop  37317  sucneqond  38397  onexgt  44351  onexomgt  44352  onexoegt  44355  onepsuc  44363  onsucelab  44374  ordnexbtwnsuc  44378  onsucrn  44382  cantnftermord  44431  cantnfub2  44433  omabs2  44443  onsucunipr  44483  onsucunitp  44484  nadd1suc  44503  naddwordnexlem0  44507  naddwordnexlem1  44508  minregex  44644  onsetreclem2  50982