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

Theorem ordsuc 6652
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 5447 . . . 4  |-  ( A  e.  _V  ->  ( A  e.  On  <->  Ord  A ) )
2 suceloni 6651 . . . . 5  |-  ( A  e.  On  ->  suc  A  e.  On )
3 eloni 5449 . . . . 5  |-  ( suc 
A  e.  On  ->  Ord 
suc  A )
42, 3syl 17 . . . 4  |-  ( A  e.  On  ->  Ord  suc 
A )
51, 4syl6bir 232 . . 3  |-  ( A  e.  _V  ->  ( Ord  A  ->  Ord  suc  A
) )
6 sucidg 5517 . . . 4  |-  ( A  e.  _V  ->  A  e.  suc  A )
7 ordelord 5461 . . . . 5  |-  ( ( Ord  suc  A  /\  A  e.  suc  A )  ->  Ord  A )
87ex 435 . . . 4  |-  ( Ord 
suc  A  ->  ( A  e.  suc  A  ->  Ord  A ) )
96, 8syl5com 31 . . 3  |-  ( A  e.  _V  ->  ( Ord  suc  A  ->  Ord  A ) )
105, 9impbid 193 . 2  |-  ( A  e.  _V  ->  ( Ord  A  <->  Ord  suc  A )
)
11 sucprc 5514 . . . 4  |-  ( -.  A  e.  _V  ->  suc 
A  =  A )
1211eqcomd 2430 . . 3  |-  ( -.  A  e.  _V  ->  A  =  suc  A )
13 ordeq 5446 . . 3  |-  ( A  =  suc  A  -> 
( Ord  A  <->  Ord  suc  A
) )
1412, 13syl 17 . 2  |-  ( -.  A  e.  _V  ->  ( Ord  A  <->  Ord  suc  A
) )
1510, 14pm2.61i 167 1  |-  ( Ord 
A  <->  Ord  suc  A )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 187    = wceq 1437    e. wcel 1868   _Vcvv 3081   Ord word 5438   Oncon0 5439   suc csuc 5441
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pr 4657  ax-un 6594
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-tr 4516  df-eprel 4761  df-po 4771  df-so 4772  df-fr 4809  df-we 4811  df-ord 5442  df-on 5443  df-suc 5445
This theorem is referenced by:  ordpwsuc  6653  sucelon  6655  ordsucss  6656  onpsssuc  6657  ordsucelsuc  6660  ordsucsssuc  6661  ordsucuniel  6662  ordsucun  6663  onsucuni2  6672  0elsuc  6673  nlimsucg  6680  limsssuc  6688  php4  7762  cantnflt  8179  fin23lem26  8756  hsmexlem1  8857  onsuct0  31094
  Copyright terms: Public domain W3C validator