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

Theorem ordsuc 6630
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 4872 . . . 4  |-  ( A  e.  _V  ->  ( A  e.  On  <->  Ord  A ) )
2 suceloni 6629 . . . . 5  |-  ( A  e.  On  ->  suc  A  e.  On )
3 eloni 4874 . . . . 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 4942 . . . 4  |-  ( A  e.  _V  ->  A  e.  suc  A )
7 ordelord 4886 . . . . 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 4939 . . . 4  |-  ( -.  A  e.  _V  ->  suc 
A  =  A )
1211eqcomd 2449 . . 3  |-  ( -.  A  e.  _V  ->  A  =  suc  A )
13 ordeq 4871 . . 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 1381    e. wcel 1802   _Vcvv 3093   Ord word 4863   Oncon0 4864   suc csuc 4866
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pr 4672  ax-un 6573
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-sbc 3312  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-pss 3474  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-tp 4015  df-op 4017  df-uni 4231  df-br 4434  df-opab 4492  df-tr 4527  df-eprel 4777  df-po 4786  df-so 4787  df-fr 4824  df-we 4826  df-ord 4867  df-on 4868  df-suc 4870
This theorem is referenced by:  ordpwsuc  6631  sucelon  6633  ordsucss  6634  onpsssuc  6635  ordsucelsuc  6638  ordsucsssuc  6639  ordsucuniel  6640  ordsucun  6641  onsucuni2  6650  0elsuc  6651  nlimsucg  6658  limsssuc  6666  php4  7702  cantnflt  8089  cantnfltOLD  8119  fin23lem26  8703  hsmexlem1  8804  onsuct0  29874
  Copyright terms: Public domain W3C validator