Theorem sucelon 7656

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 7653	. . 3 ⊢ (Ord 𝐴 ↔ Ord suc 𝐴)
2		sucexb 7646	. . 3 ⊢ (𝐴 ∈ V ↔ suc 𝐴 ∈ V)
3	1, 2	anbi12i 627	. 2 ⊢ ((Ord 𝐴 ∧ 𝐴 ∈ V) ↔ (Ord suc 𝐴 ∧ suc 𝐴 ∈ V))
4		elon2 6275	. 2 ⊢ (𝐴 ∈ On ↔ (Ord 𝐴 ∧ 𝐴 ∈ V))
5		elon2 6275	. 2 ⊢ (suc 𝐴 ∈ On ↔ (Ord suc 𝐴 ∧ suc 𝐴 ∈ V))
6	3, 4, 5	3bitr4i 303	1 ⊢ (𝐴 ∈ On ↔ suc 𝐴 ∈ On)

Syntax hints:   ↔ wb 205   ∧ wa 396   ∈ wcel 2110  Vcvv 3431  Ord word 6263  Oncon0 6264  suc csuc 6266

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-11 2158  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356  ax-un 7580

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-ne 2946  df-ral 3071  df-rex 3072  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-opab 5142  df-tr 5197  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-ord 6267  df-on 6268  df-suc 6270

This theorem is referenced by:  onsucmin  7660  tfindsg2  7700  oaordi  8360  oalimcl  8374  omlimcl  8392  omeulem1  8396  oeordsuc  8408  infensuc  8922  cantnflem1b  9420  cantnflem1  9423  r1ordg  9535  alephnbtwn  9826  cfsuc  10012  alephsuc3  10335  alephreg  10337  naddcllem  33825  bdayimaon  33890  nosupbnd1lem1  33905  nosupbnd1  33911  nosupbnd2lem1  33912  nosupbnd2  33913  noinfno  33915  noinfres  33919  noinfbnd1lem1  33920  noinfbnd1  33926  noinfbnd2lem1  33927  noinfbnd2  33928  noeta2  33973  etasslt2  34002