Theorem sucelon 7652

Description: The successor of an ordinal number is an ordinal number. (Contributed by NM, 9-Sep-2003.)

Assertion

Ref	Expression
sucelon	⊢ (𝐴 ∈ On ↔ suc 𝐴 ∈ On)

Proof of Theorem sucelon

Step	Hyp	Ref	Expression
1		ordsuc 7649	. . 3 ⊢ (Ord 𝐴 ↔ Ord suc 𝐴)
2		sucexb 7644	. . 3 ⊢ (𝐴 ∈ V ↔ suc 𝐴 ∈ V)
3	1, 2	anbi12i 626	. 2 ⊢ ((Ord 𝐴 ∧ 𝐴 ∈ V) ↔ (Ord suc 𝐴 ∧ suc 𝐴 ∈ V))
4		elon2 6274	. 2 ⊢ (𝐴 ∈ On ↔ (Ord 𝐴 ∧ 𝐴 ∈ V))
5		elon2 6274	. 2 ⊢ (suc 𝐴 ∈ On ↔ (Ord suc 𝐴 ∧ suc 𝐴 ∈ V))
6	3, 4, 5	3bitr4i 302	1 ⊢ (𝐴 ∈ On ↔ suc 𝐴 ∈ On)

Syntax hints:   ↔ wb 205   ∧ wa 395   ∈ wcel 2109  Vcvv 3430  Ord word 6262  Oncon0 6263  suc csuc 6265

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-11 2157  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355  ax-un 7579

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-ne 2945  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-pss 3910  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4845  df-br 5079  df-opab 5141  df-tr 5196  df-eprel 5494  df-po 5502  df-so 5503  df-fr 5543  df-we 5545  df-ord 6266  df-on 6267  df-suc 6269

This theorem is referenced by:  onsucmin  7656  tfindsg2  7696  oaordi  8353  oalimcl  8367  omlimcl  8385  omeulem1  8389  oeordsuc  8401  infensuc  8907  cantnflem1b  9405  cantnflem1  9408  r1ordg  9520  alephnbtwn  9811  cfsuc  9997  alephsuc3  10320  alephreg  10322  naddcllem  33810  bdayimaon  33875  nosupbnd1lem1  33890  nosupbnd1  33896  nosupbnd2lem1  33897  nosupbnd2  33898  noinfno  33900  noinfres  33904  noinfbnd1lem1  33905  noinfbnd1  33911  noinfbnd2lem1  33912  noinfbnd2  33913  noeta2  33958  etasslt2  33987