Theorem onsuc 7753

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

Syntax hints:   → wi 4   ∈ wcel 2113  Vcvv 3438  Oncon0 6315  suc csuc 6317

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 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375  ax-un 7678

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 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-tr 5204  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-ord 6318  df-on 6319  df-suc 6321

This theorem is referenced by:  unon  7771  onsuci  7779  ordunisuc2  7784  ordzsl  7785  onzsl  7786  tfindsg  7801  dfom2  7808  findsg  7837  tfrlem12  8318  oasuc  8449  omsuc  8451  onasuc  8453  oacl  8460  oneo  8506  omeulem1  8507  omeulem2  8508  oeordi  8513  oeworde  8519  oelim2  8521  oelimcl  8526  oeeulem  8527  oeeui  8528  oaabs2  8575  naddsuc2  8627  omxpenlem  9004  card2inf  9458  cantnflt  9579  cantnflem1d  9595  cnfcom  9607  r1ordg  9688  bndrank  9751  r1pw  9755  r1pwALT  9756  tcrank  9794  onssnum  9948  dfac12lem2  10053  cfsuc  10165  cfsmolem  10178  fin1a2lem1  10308  fin1a2lem2  10309  ttukeylem7  10423  alephreg  10491  gch2  10584  winainflem  10602  winalim2  10605  r1wunlim  10646  nqereu  10838  noextend  27632  noresle  27663  nosupno  27669  madeoldsuc  27857  bdayn0p1  28327  constrextdg2lem  33854  fineqvnttrclselem2  35227  ontgval  36574  ontgsucval  36575  onsuctop  36576  sucneqond  37509  onexgt  43424  onexomgt  43425  onexoegt  43428  onepsuc  43436  onsucelab  43447  ordnexbtwnsuc  43451  onsucrn  43455  cantnftermord  43504  cantnfub2  43506  omabs2  43516  onsucunipr  43556  onsucunitp  43557  nadd1suc  43576  naddwordnexlem0  43580  naddwordnexlem1  43581  minregex  43717  onsetreclem2  49893