Theorem onsuc 7822

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3451  Oncon0 6361  suc csuc 6363

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391  ax-un 7749

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-tr 5213  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6364  df-on 6365  df-suc 6367

This theorem is used by:  unon  7840  onsuci  7848  ordunisuc2  7853  ordzsl  7854  onzsl  7855  tfindsg  7870  dfom2  7877  findsg  7907  tfrlem12  8390  oasuc  8525  omsuc  8527  onasuc  8529  oacl  8536  oneo  8582  omeulem1  8583  omeulem2  8584  oeordi  8589  oeworde  8595  oelim2  8597  oelimcl  8602  oeeulem  8603  oeeui  8604  oaabs2  8651  naddsuc2  8704  omxpenlem  9090  card2inf  9542  cantnflt  9666  cantnflem1d  9682  cnfcom  9694  r1ordg  9778  bndrank  9847  r1pw  9852  r1pwALT  9853  tcrank  9894  onssnum  10112  dfac12lem2  10216  cfsuc  10328  cfsmolem  10341  fin1a2lem1  10471  fin1a2lem2  10472  ttukeylem7  10586  alephreg  10660  gch2  10753  winainflem  10771  winalim2  10774  r1wunlim  10815  nqereu  11007  noextend  28016  noresle  28047  nosupno  28053  madeoldsuc  28264  bdayn0p1  28748  constrextdg2lem  34373  fineqvnttrclselem2  35773  nmulprop  36919  ontgval  37199  ontgsucval  37200  onsuctop  37201  sucneqond  38268  onexgt  44226  onexomgt  44227  onexoegt  44230  onepsuc  44238  onsucelab  44249  ordnexbtwnsuc  44253  onsucrn  44257  cantnftermord  44306  cantnfub2  44308  omabs2  44318  onsucunipr  44358  onsucunitp  44359  nadd1suc  44378  naddwordnexlem0  44382  naddwordnexlem1  44383  minregex  44519  onsetreclem2  50768