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

Theorem suceloni 4620
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 4450 . . . . . . . 8  |-  ( A  e.  On  ->  (
x  e.  A  ->  x  C_  A ) )
2 elsn 3668 . . . . . . . . . 10  |-  ( x  e.  { A }  <->  x  =  A )
3 eqimss 3243 . . . . . . . . . 10  |-  ( x  =  A  ->  x  C_  A )
42, 3sylbi 187 . . . . . . . . 9  |-  ( x  e.  { A }  ->  x  C_  A )
54a1i 10 . . . . . . . 8  |-  ( A  e.  On  ->  (
x  e.  { A }  ->  x  C_  A
) )
61, 5orim12d 811 . . . . . . 7  |-  ( A  e.  On  ->  (
( x  e.  A  \/  x  e.  { A } )  ->  (
x  C_  A  \/  x  C_  A ) ) )
7 df-suc 4414 . . . . . . . . 9  |-  suc  A  =  ( A  u.  { A } )
87eleq2i 2360 . . . . . . . 8  |-  ( x  e.  suc  A  <->  x  e.  ( A  u.  { A } ) )
9 elun 3329 . . . . . . . 8  |-  ( x  e.  ( A  u.  { A } )  <->  ( x  e.  A  \/  x  e.  { A } ) )
108, 9bitr2i 241 . . . . . . 7  |-  ( ( x  e.  A  \/  x  e.  { A } )  <->  x  e.  suc  A )
11 oridm 500 . . . . . . 7  |-  ( ( x  C_  A  \/  x  C_  A )  <->  x  C_  A
)
126, 10, 113imtr3g 260 . . . . . 6  |-  ( A  e.  On  ->  (
x  e.  suc  A  ->  x  C_  A )
)
13 sssucid 4485 . . . . . 6  |-  A  C_  suc  A
14 sstr2 3199 . . . . . 6  |-  ( x 
C_  A  ->  ( A  C_  suc  A  ->  x  C_  suc  A ) )
1512, 13, 14syl6mpi 58 . . . . 5  |-  ( A  e.  On  ->  (
x  e.  suc  A  ->  x  C_  suc  A ) )
1615ralrimiv 2638 . . . 4  |-  ( A  e.  On  ->  A. x  e.  suc  A x  C_  suc  A )
17 dftr3 4133 . . . 4  |-  ( Tr 
suc  A  <->  A. x  e.  suc  A x  C_  suc  A )
1816, 17sylibr 203 . . 3  |-  ( A  e.  On  ->  Tr  suc  A )
19 onss 4598 . . . . 5  |-  ( A  e.  On  ->  A  C_  On )
20 snssi 3775 . . . . 5  |-  ( A  e.  On  ->  { A }  C_  On )
2119, 20unssd 3364 . . . 4  |-  ( A  e.  On  ->  ( A  u.  { A } )  C_  On )
227, 21syl5eqss 3235 . . 3  |-  ( A  e.  On  ->  suc  A 
C_  On )
23 ordon 4590 . . . 4  |-  Ord  On
24 trssord 4425 . . . . 5  |-  ( ( Tr  suc  A  /\  suc  A  C_  On  /\  Ord  On )  ->  Ord  suc  A
)
25243exp 1150 . . . 4  |-  ( Tr 
suc  A  ->  ( suc 
A  C_  On  ->  ( Ord  On  ->  Ord  suc 
A ) ) )
2623, 25mpii 39 . . 3  |-  ( Tr 
suc  A  ->  ( suc 
A  C_  On  ->  Ord 
suc  A ) )
2718, 22, 26sylc 56 . 2  |-  ( A  e.  On  ->  Ord  suc 
A )
28 sucexg 4617 . . 3  |-  ( A  e.  On  ->  suc  A  e.  _V )
29 elong 4416 . . 3  |-  ( suc 
A  e.  _V  ->  ( suc  A  e.  On  <->  Ord 
suc  A ) )
3028, 29syl 15 . 2  |-  ( A  e.  On  ->  ( suc  A  e.  On  <->  Ord  suc  A
) )
3127, 30mpbird 223 1  |-  ( A  e.  On  ->  suc  A  e.  On )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    \/ wo 357    = wceq 1632    e. wcel 1696   A.wral 2556   _Vcvv 2801    u. cun 3163    C_ wss 3165   {csn 3653   Tr wtr 4129   Ord word 4407   Oncon0 4408   suc csuc 4410
This theorem is referenced by:  ordsuc  4621  unon  4638  onsuci  4645  ordunisuc2  4651  ordzsl  4652  onzsl  4653  tfindsg  4667  dfom2  4674  findsg  4699  tfrlem12  6421  oasuc  6539  omsuc  6541  onasuc  6543  oacl  6550  oneo  6595  omeulem1  6596  omeulem2  6597  oeordi  6601  oeworde  6607  oelim2  6609  oelimcl  6614  oeeulem  6615  oeeui  6616  oaabs2  6659  omxpenlem  6979  card2inf  7285  cantnflt  7389  cantnflem1d  7406  cnfcom  7419  r1ordg  7466  bndrank  7529  r1pw  7533  r1pwOLD  7534  tcrank  7570  onssnum  7683  dfac12lem2  7786  cfsuc  7899  cfsmolem  7912  fin1a2lem1  8042  fin1a2lem2  8043  ttukeylem7  8158  alephreg  8220  gch2  8317  winainflem  8331  winalim2  8334  r1wunlim  8375  nqereu  8569  ontgval  24942  ontgsucval  24943  onsuctop  24944
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pr 4230  ax-un 4528
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-sbc 3005  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-pss 3181  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-tp 3661  df-op 3662  df-uni 3844  df-br 4040  df-opab 4094  df-tr 4130  df-eprel 4321  df-po 4330  df-so 4331  df-fr 4368  df-we 4370  df-ord 4411  df-on 4412  df-suc 4414
  Copyright terms: Public domain W3C validator