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

Theorem suceloni 6629
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 4906 . . . . . . . 8  |-  ( A  e.  On  ->  (
x  e.  A  ->  x  C_  A ) )
2 elsn 4024 . . . . . . . . . 10  |-  ( x  e.  { A }  <->  x  =  A )
3 eqimss 3538 . . . . . . . . . 10  |-  ( x  =  A  ->  x  C_  A )
42, 3sylbi 195 . . . . . . . . 9  |-  ( x  e.  { A }  ->  x  C_  A )
54a1i 11 . . . . . . . 8  |-  ( A  e.  On  ->  (
x  e.  { A }  ->  x  C_  A
) )
61, 5orim12d 836 . . . . . . 7  |-  ( A  e.  On  ->  (
( x  e.  A  \/  x  e.  { A } )  ->  (
x  C_  A  \/  x  C_  A ) ) )
7 df-suc 4870 . . . . . . . . 9  |-  suc  A  =  ( A  u.  { A } )
87eleq2i 2519 . . . . . . . 8  |-  ( x  e.  suc  A  <->  x  e.  ( A  u.  { A } ) )
9 elun 3627 . . . . . . . 8  |-  ( x  e.  ( A  u.  { A } )  <->  ( x  e.  A  \/  x  e.  { A } ) )
108, 9bitr2i 250 . . . . . . 7  |-  ( ( x  e.  A  \/  x  e.  { A } )  <->  x  e.  suc  A )
11 oridm 514 . . . . . . 7  |-  ( ( x  C_  A  \/  x  C_  A )  <->  x  C_  A
)
126, 10, 113imtr3g 269 . . . . . 6  |-  ( A  e.  On  ->  (
x  e.  suc  A  ->  x  C_  A )
)
13 sssucid 4941 . . . . . 6  |-  A  C_  suc  A
14 sstr2 3493 . . . . . 6  |-  ( x 
C_  A  ->  ( A  C_  suc  A  ->  x  C_  suc  A ) )
1512, 13, 14syl6mpi 62 . . . . 5  |-  ( A  e.  On  ->  (
x  e.  suc  A  ->  x  C_  suc  A ) )
1615ralrimiv 2853 . . . 4  |-  ( A  e.  On  ->  A. x  e.  suc  A x  C_  suc  A )
17 dftr3 4530 . . . 4  |-  ( Tr 
suc  A  <->  A. x  e.  suc  A x  C_  suc  A )
1816, 17sylibr 212 . . 3  |-  ( A  e.  On  ->  Tr  suc  A )
19 onss 6607 . . . . 5  |-  ( A  e.  On  ->  A  C_  On )
20 snssi 4155 . . . . 5  |-  ( A  e.  On  ->  { A }  C_  On )
2119, 20unssd 3662 . . . 4  |-  ( A  e.  On  ->  ( A  u.  { A } )  C_  On )
227, 21syl5eqss 3530 . . 3  |-  ( A  e.  On  ->  suc  A 
C_  On )
23 ordon 6599 . . . 4  |-  Ord  On
24 trssord 4881 . . . . 5  |-  ( ( Tr  suc  A  /\  suc  A  C_  On  /\  Ord  On )  ->  Ord  suc  A
)
25243exp 1194 . . . 4  |-  ( Tr 
suc  A  ->  ( suc 
A  C_  On  ->  ( Ord  On  ->  Ord  suc 
A ) ) )
2623, 25mpii 43 . . 3  |-  ( Tr 
suc  A  ->  ( suc 
A  C_  On  ->  Ord 
suc  A ) )
2718, 22, 26sylc 60 . 2  |-  ( A  e.  On  ->  Ord  suc 
A )
28 sucexg 6626 . . 3  |-  ( A  e.  On  ->  suc  A  e.  _V )
29 elong 4872 . . 3  |-  ( suc 
A  e.  _V  ->  ( suc  A  e.  On  <->  Ord 
suc  A ) )
3028, 29syl 16 . 2  |-  ( A  e.  On  ->  ( suc  A  e.  On  <->  Ord  suc  A
) )
3127, 30mpbird 232 1  |-  ( A  e.  On  ->  suc  A  e.  On )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    \/ wo 368    = wceq 1381    e. wcel 1802   A.wral 2791   _Vcvv 3093    u. cun 3456    C_ wss 3458   {csn 4010   Tr wtr 4526   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:  ordsuc  6630  unon  6647  onsuci  6654  ordunisuc2  6660  ordzsl  6661  onzsl  6662  tfindsg  6676  dfom2  6683  findsg  6708  tfrlem12  7056  oasuc  7172  omsuc  7174  onasuc  7176  oacl  7183  oneo  7228  omeulem1  7229  omeulem2  7230  oeordi  7234  oeworde  7240  oelim2  7242  oelimcl  7247  oeeulem  7248  oeeui  7249  oaabs2  7292  omxpenlem  7616  card2inf  7979  cantnflt  8089  cantnflem1d  8105  cantnfltOLD  8119  cantnflem1dOLD  8128  cnfcom  8142  cnfcomOLD  8150  r1ordg  8194  bndrank  8257  r1pw  8261  r1pwOLD  8262  tcrank  8300  onssnum  8419  dfac12lem2  8522  cfsuc  8635  cfsmolem  8648  fin1a2lem1  8778  fin1a2lem2  8779  ttukeylem7  8893  alephreg  8955  gch2  9051  winainflem  9069  winalim2  9072  r1wunlim  9113  nqereu  9305  ontgval  29864  ontgsucval  29865  onsuctop  29866
  Copyright terms: Public domain W3C validator