Theorem onsuc 7755

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

Syntax hints:   → wi 4   ∈ wcel 2113  Vcvv 3440  Oncon0 6317  suc csuc 6319

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 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680

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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-tr 5206  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-ord 6320  df-on 6321  df-suc 6323

This theorem is referenced by:  unon  7773  onsuci  7781  ordunisuc2  7786  ordzsl  7787  onzsl  7788  tfindsg  7803  dfom2  7810  findsg  7839  tfrlem12  8320  oasuc  8451  omsuc  8453  onasuc  8455  oacl  8462  oneo  8508  omeulem1  8509  omeulem2  8510  oeordi  8515  oeworde  8521  oelim2  8523  oelimcl  8528  oeeulem  8529  oeeui  8530  oaabs2  8577  naddsuc2  8629  omxpenlem  9006  card2inf  9460  cantnflt  9581  cantnflem1d  9597  cnfcom  9609  r1ordg  9690  bndrank  9753  r1pw  9757  r1pwALT  9758  tcrank  9796  onssnum  9950  dfac12lem2  10055  cfsuc  10167  cfsmolem  10180  fin1a2lem1  10310  fin1a2lem2  10311  ttukeylem7  10425  alephreg  10493  gch2  10586  winainflem  10604  winalim2  10607  r1wunlim  10648  nqereu  10840  noextend  27634  noresle  27665  nosupno  27671  madeoldsuc  27881  bdayn0p1  28365  constrextdg2lem  33905  fineqvnttrclselem2  35278  ontgval  36625  ontgsucval  36626  onsuctop  36627  sucneqond  37570  onexgt  43482  onexomgt  43483  onexoegt  43486  onepsuc  43494  onsucelab  43505  ordnexbtwnsuc  43509  onsucrn  43513  cantnftermord  43562  cantnfub2  43564  omabs2  43574  onsucunipr  43614  onsucunitp  43615  nadd1suc  43634  naddwordnexlem0  43638  naddwordnexlem1  43639  minregex  43775  onsetreclem2  49951