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

Theorem suceloni 6652
Description: The successor of an ordinal number is an ordinal number. Proposition 7.24 of [TakeutiZaring] p. 41. (Contributed by NM, 6-Jun-1994.)
Assertion
Ref Expression
suceloni  |-  ( A  e.  On  ->  suc  A  e.  On )

Proof of Theorem suceloni
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 onelss 5482 . . . . . . . 8  |-  ( A  e.  On  ->  (
x  e.  A  ->  x  C_  A ) )
2 elsn 4011 . . . . . . . . . 10  |-  ( x  e.  { A }  <->  x  =  A )
3 eqimss 3517 . . . . . . . . . 10  |-  ( x  =  A  ->  x  C_  A )
42, 3sylbi 199 . . . . . . . . 9  |-  ( x  e.  { A }  ->  x  C_  A )
54a1i 11 . . . . . . . 8  |-  ( A  e.  On  ->  (
x  e.  { A }  ->  x  C_  A
) )
61, 5orim12d 847 . . . . . . 7  |-  ( A  e.  On  ->  (
( x  e.  A  \/  x  e.  { A } )  ->  (
x  C_  A  \/  x  C_  A ) ) )
7 df-suc 5446 . . . . . . . . 9  |-  suc  A  =  ( A  u.  { A } )
87eleq2i 2501 . . . . . . . 8  |-  ( x  e.  suc  A  <->  x  e.  ( A  u.  { A } ) )
9 elun 3607 . . . . . . . 8  |-  ( x  e.  ( A  u.  { A } )  <->  ( x  e.  A  \/  x  e.  { A } ) )
108, 9bitr2i 254 . . . . . . 7  |-  ( ( x  e.  A  \/  x  e.  { A } )  <->  x  e.  suc  A )
11 oridm 517 . . . . . . 7  |-  ( ( x  C_  A  \/  x  C_  A )  <->  x  C_  A
)
126, 10, 113imtr3g 273 . . . . . 6  |-  ( A  e.  On  ->  (
x  e.  suc  A  ->  x  C_  A )
)
13 sssucid 5517 . . . . . 6  |-  A  C_  suc  A
14 sstr2 3472 . . . . . 6  |-  ( x 
C_  A  ->  ( A  C_  suc  A  ->  x  C_  suc  A ) )
1512, 13, 14syl6mpi 65 . . . . 5  |-  ( A  e.  On  ->  (
x  e.  suc  A  ->  x  C_  suc  A ) )
1615ralrimiv 2838 . . . 4  |-  ( A  e.  On  ->  A. x  e.  suc  A x  C_  suc  A )
17 dftr3 4520 . . . 4  |-  ( Tr 
suc  A  <->  A. x  e.  suc  A x  C_  suc  A )
1816, 17sylibr 216 . . 3  |-  ( A  e.  On  ->  Tr  suc  A )
19 onss 6629 . . . . 5  |-  ( A  e.  On  ->  A  C_  On )
20 snssi 4142 . . . . 5  |-  ( A  e.  On  ->  { A }  C_  On )
2119, 20unssd 3643 . . . 4  |-  ( A  e.  On  ->  ( A  u.  { A } )  C_  On )
227, 21syl5eqss 3509 . . 3  |-  ( A  e.  On  ->  suc  A 
C_  On )
23 ordon 6621 . . . 4  |-  Ord  On
24 trssord 5457 . . . . 5  |-  ( ( Tr  suc  A  /\  suc  A  C_  On  /\  Ord  On )  ->  Ord  suc  A
)
25243exp 1205 . . . 4  |-  ( Tr 
suc  A  ->  ( suc 
A  C_  On  ->  ( Ord  On  ->  Ord  suc 
A ) ) )
2623, 25mpii 45 . . 3  |-  ( Tr 
suc  A  ->  ( suc 
A  C_  On  ->  Ord 
suc  A ) )
2718, 22, 26sylc 63 . 2  |-  ( A  e.  On  ->  Ord  suc 
A )
28 sucexg 6649 . . 3  |-  ( A  e.  On  ->  suc  A  e.  _V )
29 elong 5448 . . 3  |-  ( suc 
A  e.  _V  ->  ( suc  A  e.  On  <->  Ord 
suc  A ) )
3028, 29syl 17 . 2  |-  ( A  e.  On  ->  ( suc  A  e.  On  <->  Ord  suc  A
) )
3127, 30mpbird 236 1  |-  ( A  e.  On  ->  suc  A  e.  On )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    \/ wo 370    = wceq 1438    e. wcel 1869   A.wral 2776   _Vcvv 3082    u. cun 3435    C_ wss 3437   {csn 3997   Tr wtr 4516   Ord word 5439   Oncon0 5440   suc csuc 5442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pr 4658  ax-un 6595
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 984  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3084  df-sbc 3301  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-pss 3453  df-nul 3763  df-if 3911  df-sn 3998  df-pr 4000  df-tp 4002  df-op 4004  df-uni 4218  df-br 4422  df-opab 4481  df-tr 4517  df-eprel 4762  df-po 4772  df-so 4773  df-fr 4810  df-we 4812  df-ord 5443  df-on 5444  df-suc 5446
This theorem is referenced by:  ordsuc  6653  unon  6670  onsuci  6677  ordunisuc2  6683  ordzsl  6684  onzsl  6685  tfindsg  6699  dfom2  6706  findsg  6732  tfrlem12  7113  oasuc  7232  omsuc  7234  onasuc  7236  oacl  7243  oneo  7288  omeulem1  7289  omeulem2  7290  oeordi  7294  oeworde  7300  oelim2  7302  oelimcl  7307  oeeulem  7308  oeeui  7309  oaabs2  7352  omxpenlem  7677  card2inf  8074  cantnflt  8180  cantnflem1d  8196  cnfcom  8208  r1ordg  8252  bndrank  8315  r1pw  8319  r1pwALT  8320  tcrank  8358  onssnum  8473  dfac12lem2  8576  cfsuc  8689  cfsmolem  8702  fin1a2lem1  8832  fin1a2lem2  8833  ttukeylem7  8947  alephreg  9009  gch2  9102  winainflem  9120  winalim2  9123  r1wunlim  9164  nqereu  9356  ontgval  31090  ontgsucval  31091  onsuctop  31092  sucneqond  31726
  Copyright terms: Public domain W3C validator