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

Theorem suceloni 4604
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 )
Dummy variable  x is distinct from all other variables.

Proof of Theorem suceloni
StepHypRef Expression
1 onelss 4434 . . . . . . . 8  |-  ( A  e.  On  ->  (
x  e.  A  ->  x  C_  A ) )
2 elsn 3657 . . . . . . . . . 10  |-  ( x  e.  { A }  <->  x  =  A )
3 eqimss 3232 . . . . . . . . . 10  |-  ( x  =  A  ->  x  C_  A )
42, 3sylbi 189 . . . . . . . . 9  |-  ( x  e.  { A }  ->  x  C_  A )
54a1i 12 . . . . . . . 8  |-  ( A  e.  On  ->  (
x  e.  { A }  ->  x  C_  A
) )
61, 5orim12d 813 . . . . . . 7  |-  ( A  e.  On  ->  (
( x  e.  A  \/  x  e.  { A } )  ->  (
x  C_  A  \/  x  C_  A ) ) )
7 df-suc 4398 . . . . . . . . 9  |-  suc  A  =  ( A  u.  { A } )
87eleq2i 2349 . . . . . . . 8  |-  ( x  e.  suc  A  <->  x  e.  ( A  u.  { A } ) )
9 elun 3318 . . . . . . . 8  |-  ( x  e.  ( A  u.  { A } )  <->  ( x  e.  A  \/  x  e.  { A } ) )
108, 9bitr2i 243 . . . . . . 7  |-  ( ( x  e.  A  \/  x  e.  { A } )  <->  x  e.  suc  A )
11 oridm 502 . . . . . . 7  |-  ( ( x  C_  A  \/  x  C_  A )  <->  x  C_  A
)
126, 10, 113imtr3g 262 . . . . . 6  |-  ( A  e.  On  ->  (
x  e.  suc  A  ->  x  C_  A )
)
13 sssucid 4469 . . . . . 6  |-  A  C_  suc  A
14 sstr2 3188 . . . . . 6  |-  ( x 
C_  A  ->  ( A  C_  suc  A  ->  x  C_  suc  A ) )
1512, 13, 14syl6mpi 60 . . . . 5  |-  ( A  e.  On  ->  (
x  e.  suc  A  ->  x  C_  suc  A ) )
1615ralrimiv 2627 . . . 4  |-  ( A  e.  On  ->  A. x  e.  suc  A x  C_  suc  A )
17 dftr3 4119 . . . 4  |-  ( Tr 
suc  A  <->  A. x  e.  suc  A x  C_  suc  A )
1816, 17sylibr 205 . . 3  |-  ( A  e.  On  ->  Tr  suc  A )
19 onss 4582 . . . . 5  |-  ( A  e.  On  ->  A  C_  On )
20 snssi 3761 . . . . 5  |-  ( A  e.  On  ->  { A }  C_  On )
2119, 20unssd 3353 . . . 4  |-  ( A  e.  On  ->  ( A  u.  { A } )  C_  On )
227, 21syl5eqss 3224 . . 3  |-  ( A  e.  On  ->  suc  A 
C_  On )
23 ordon 4574 . . . 4  |-  Ord  On
24 trssord 4409 . . . . 5  |-  ( ( Tr  suc  A  /\  suc  A  C_  On  /\  Ord  On )  ->  Ord  suc  A
)
25243exp 1152 . . . 4  |-  ( Tr 
suc  A  ->  ( suc 
A  C_  On  ->  ( Ord  On  ->  Ord  suc 
A ) ) )
2623, 25mpii 41 . . 3  |-  ( Tr 
suc  A  ->  ( suc 
A  C_  On  ->  Ord 
suc  A ) )
2718, 22, 26sylc 58 . 2  |-  ( A  e.  On  ->  Ord  suc 
A )
28 sucexg 4601 . . 3  |-  ( A  e.  On  ->  suc  A  e.  _V )
29 elong 4400 . . 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 225 1  |-  ( A  e.  On  ->  suc  A  e.  On )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    \/ wo 359    = wceq 1624    e. wcel 1685   A.wral 2545   _Vcvv 2790    u. cun 3152    C_ wss 3154   {csn 3642   Tr wtr 4115   Ord word 4391   Oncon0 4392   suc csuc 4394
This theorem is referenced by:  ordsuc  4605  unon  4622  onsuci  4629  ordunisuc2  4635  ordzsl  4636  onzsl  4637  tfindsg  4651  dfom2  4658  findsg  4683  tfrlem12  6401  oasuc  6519  omsuc  6521  onasuc  6523  oacl  6530  oneo  6575  omeulem1  6576  omeulem2  6577  oeordi  6581  oeworde  6587  oelim2  6589  oelimcl  6594  oeeulem  6595  oeeui  6596  oaabs2  6639  omxpenlem  6959  card2inf  7265  cantnflt  7369  cantnflem1d  7386  cnfcom  7399  r1ordg  7446  bndrank  7509  r1pw  7513  r1pwOLD  7514  tcrank  7550  onssnum  7663  dfac12lem2  7766  cfsuc  7879  cfsmolem  7892  fin1a2lem1  8022  fin1a2lem2  8023  ttukeylem7  8138  alephreg  8200  gch2  8297  winainflem  8311  winalim2  8314  r1wunlim  8355  nqereu  8549  ontgval  24278  ontgsucval  24279  onsuctop  24280
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pr 4214  ax-un 4512
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 937  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-sbc 2994  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-pss 3170  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-tp 3650  df-op 3651  df-uni 3830  df-br 4026  df-opab 4080  df-tr 4116  df-eprel 4305  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396  df-suc 4398
  Copyright terms: Public domain W3C validator