Theorem onsuc 7858

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  Vcvv 3454  Oncon0 6388  suc csuc 6390

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pr 5398  ax-un 7783

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-tr 5219  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-ord 6391  df-on 6392  df-suc 6394

This theorem is used by:  unon  7876  onsuci  7884  ordunisuc2  7889  ordzsl  7890  onzsl  7891  tfindsg  7906  dfom2  7913  findsg  7943  tfrlem12  8435  oasuc  8570  omsuc  8572  onasuc  8574  oacl  8581  oneo  8627  omeulem1  8628  omeulem2  8629  oeordi  8634  oeworde  8640  oelim2  8642  oelimcl  8647  oeeulem  8648  oeeui  8649  oaabs2  8696  naddsuc2  8749  omxpenlem  9135  card2inf  9586  cantnflt  9710  cantnflem1d  9726  cnfcom  9738  r1ordg  9822  bndrank  9891  r1pw  9896  r1pwALT  9897  tcrank  9938  onssnum  10158  dfac12lem2  10262  cfsuc  10374  cfsmolem  10387  fin1a2lem1  10517  fin1a2lem2  10518  ttukeylem7  10632  alephreg  10706  gch2  10799  winainflem  10817  winalim2  10820  r1wunlim  10861  nqereu  11053  noextend  28080  noresle  28111  nosupno  28117  madeoldsuc  28328  bdayn0p1  28812  constrextdg2lem  34491  fineqvnttrclselem2  35931  j0ltalephlem  36048  j0ltaleph  36049  nmulprop  37154  ontgval  37434  ontgsucval  37435  onsuctop  37436  sucneqond  38556  onexgt  44503  onexomgt  44504  onexoegt  44507  onepsuc  44515  onsucelab  44526  ordnexbtwnsuc  44530  onsucrn  44534  cantnftermord  44583  cantnfub2  44585  omabs2  44595  onsucunipr  44635  onsucunitp  44636  nadd1suc  44655  naddwordnexlem0  44659  naddwordnexlem1  44660  minregex  44796  onsetreclem2  51205