Theorem onsuc 7809

Description: The successor of an ordinal number is an ordinal number. Closed form of onsuci 7835. Forward implication of onsucb 7813. 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 7804	. 2 ⊢ (𝐴 ∈ On → suc 𝐴 ∈ V)
2		sucexeloni 7808	. 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 3450  Oncon0 6357  suc csuc 6359

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 2732  ax-sep 5251  ax-pr 5398  ax-un 7736

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 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-ord 6360  df-on 6361  df-suc 6363

This theorem is used by:  unon  7827  onsuci  7835  ordunisuc2  7840  ordzsl  7841  onzsl  7842  tfindsg  7857  dfom2  7864  findsg  7894  tfrlem12  8378  oasuc  8511  omsuc  8513  onasuc  8515  oacl  8522  oneo  8568  omeulem1  8569  omeulem2  8570  oeordi  8575  oeworde  8581  oelim2  8583  oelimcl  8588  oeeulem  8589  oeeui  8590  oaabs2  8637  naddsuc2  8690  omxpenlem  9076  card2inf  9527  cantnflt  9651  cantnflem1d  9667  cnfcom  9679  r1ordg  9760  bndrank  9823  r1pw  9827  r1pwALT  9828  tcrank  9866  onssnum  10043  dfac12lem2  10147  cfsuc  10259  cfsmolem  10272  fin1a2lem1  10402  fin1a2lem2  10403  ttukeylem7  10517  alephreg  10591  gch2  10684  winainflem  10702  winalim2  10705  r1wunlim  10746  nqereu  10938  noextend  27902  noresle  27933  nosupno  27939  madeoldsuc  28150  bdayn0p1  28634  constrextdg2lem  34258  fineqvnttrclselem2  35648  nmulprop  36770  ontgval  37050  ontgsucval  37051  onsuctop  37052  sucneqond  38119  onexgt  44081  onexomgt  44082  onexoegt  44085  onepsuc  44093  onsucelab  44104  ordnexbtwnsuc  44108  onsucrn  44112  cantnftermord  44161  cantnfub2  44163  omabs2  44173  onsucunipr  44213  onsucunitp  44214  nadd1suc  44233  naddwordnexlem0  44237  naddwordnexlem1  44238  minregex  44374  onsetreclem2  50632