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

Theorem ordsuc 6511
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 4811 . . . 4  |-  ( A  e.  _V  ->  ( A  e.  On  <->  Ord  A ) )
2 suceloni 6510 . . . . 5  |-  ( A  e.  On  ->  suc  A  e.  On )
3 eloni 4813 . . . . 5  |-  ( suc 
A  e.  On  ->  Ord 
suc  A )
42, 3syl 16 . . . 4  |-  ( A  e.  On  ->  Ord  suc 
A )
51, 4syl6bir 229 . . 3  |-  ( A  e.  _V  ->  ( Ord  A  ->  Ord  suc  A
) )
6 sucidg 4881 . . . 4  |-  ( A  e.  _V  ->  A  e.  suc  A )
7 ordelord 4825 . . . . 5  |-  ( ( Ord  suc  A  /\  A  e.  suc  A )  ->  Ord  A )
87ex 434 . . . 4  |-  ( Ord 
suc  A  ->  ( A  e.  suc  A  ->  Ord  A ) )
96, 8syl5com 30 . . 3  |-  ( A  e.  _V  ->  ( Ord  suc  A  ->  Ord  A ) )
105, 9impbid 191 . 2  |-  ( A  e.  _V  ->  ( Ord  A  <->  Ord  suc  A )
)
11 sucprc 4878 . . . 4  |-  ( -.  A  e.  _V  ->  suc 
A  =  A )
1211eqcomd 2457 . . 3  |-  ( -.  A  e.  _V  ->  A  =  suc  A )
13 ordeq 4810 . . 3  |-  ( A  =  suc  A  -> 
( Ord  A  <->  Ord  suc  A
) )
1412, 13syl 16 . 2  |-  ( -.  A  e.  _V  ->  ( Ord  A  <->  Ord  suc  A
) )
1510, 14pm2.61i 164 1  |-  ( Ord 
A  <->  Ord  suc  A )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184    = wceq 1370    e. wcel 1757   _Vcvv 3054   Ord word 4802   Oncon0 4803   suc csuc 4805
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-sep 4497  ax-nul 4505  ax-pr 4615  ax-un 6458
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-eu 2263  df-mo 2264  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-ral 2797  df-rex 2798  df-rab 2801  df-v 3056  df-sbc 3271  df-dif 3415  df-un 3417  df-in 3419  df-ss 3426  df-pss 3428  df-nul 3722  df-if 3876  df-sn 3962  df-pr 3964  df-tp 3966  df-op 3968  df-uni 4176  df-br 4377  df-opab 4435  df-tr 4470  df-eprel 4716  df-po 4725  df-so 4726  df-fr 4763  df-we 4765  df-ord 4806  df-on 4807  df-suc 4809
This theorem is referenced by:  ordpwsuc  6512  sucelon  6514  ordsucss  6515  onpsssuc  6516  ordsucelsuc  6519  ordsucsssuc  6520  ordsucuniel  6521  ordsucun  6522  onsucuni2  6531  0elsuc  6532  nlimsucg  6539  limsssuc  6547  php4  7584  cantnflt  7967  cantnfltOLD  7997  fin23lem26  8581  hsmexlem1  8682  onsuct0  28407
  Copyright terms: Public domain W3C validator