MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ordsuc Unicode version

Theorem ordsuc 4687
Description: The successor of an ordinal class is ordinal. (Contributed by NM, 3-Apr-1995.)
Assertion
Ref Expression
ordsuc  |-  ( Ord 
A  <->  Ord  suc  A )

Proof of Theorem ordsuc
StepHypRef Expression
1 elong 4482 . . . 4  |-  ( A  e.  _V  ->  ( A  e.  On  <->  Ord  A ) )
2 suceloni 4686 . . . . 5  |-  ( A  e.  On  ->  suc  A  e.  On )
3 eloni 4484 . . . . 5  |-  ( suc 
A  e.  On  ->  Ord 
suc  A )
42, 3syl 15 . . . 4  |-  ( A  e.  On  ->  Ord  suc 
A )
51, 4syl6bir 220 . . 3  |-  ( A  e.  _V  ->  ( Ord  A  ->  Ord  suc  A
) )
6 sucidg 4552 . . . 4  |-  ( A  e.  _V  ->  A  e.  suc  A )
7 ordelord 4496 . . . . 5  |-  ( ( Ord  suc  A  /\  A  e.  suc  A )  ->  Ord  A )
87ex 423 . . . 4  |-  ( Ord 
suc  A  ->  ( A  e.  suc  A  ->  Ord  A ) )
96, 8syl5com 26 . . 3  |-  ( A  e.  _V  ->  ( Ord  suc  A  ->  Ord  A ) )
105, 9impbid 183 . 2  |-  ( A  e.  _V  ->  ( Ord  A  <->  Ord  suc  A )
)
11 sucprc 4549 . . . 4  |-  ( -.  A  e.  _V  ->  suc 
A  =  A )
1211eqcomd 2363 . . 3  |-  ( -.  A  e.  _V  ->  A  =  suc  A )
13 ordeq 4481 . . 3  |-  ( A  =  suc  A  -> 
( Ord  A  <->  Ord  suc  A
) )
1412, 13syl 15 . 2  |-  ( -.  A  e.  _V  ->  ( Ord  A  <->  Ord  suc  A
) )
1510, 14pm2.61i 156 1  |-  ( Ord 
A  <->  Ord  suc  A )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176    = wceq 1642    e. wcel 1710   _Vcvv 2864   Ord word 4473   Oncon0 4474   suc csuc 4476
This theorem is referenced by:  ordpwsuc  4688  sucelon  4690  ordsucss  4691  onpsssuc  4692  ordsucelsuc  4695  ordsucsssuc  4696  ordsucuniel  4697  ordsucun  4698  onsucuni2  4707  0elsuc  4708  nlimsucg  4715  limsssuc  4723  php4  7136  cantnflt  7463  fin23lem26  8041  hsmexlem1  8142  onsuct0  25439
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4222  ax-nul 4230  ax-pr 4295  ax-un 4594
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-sbc 3068  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-pss 3244  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-tp 3724  df-op 3725  df-uni 3909  df-br 4105  df-opab 4159  df-tr 4195  df-eprel 4387  df-po 4396  df-so 4397  df-fr 4434  df-we 4436  df-ord 4477  df-on 4478  df-suc 4480
  Copyright terms: Public domain W3C validator