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

Theorem suceloni 6565
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 4847 . . . . . . . 8  |-  ( A  e.  On  ->  (
x  e.  A  ->  x  C_  A ) )
2 elsn 3971 . . . . . . . . . 10  |-  ( x  e.  { A }  <->  x  =  A )
3 eqimss 3482 . . . . . . . . . 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 4811 . . . . . . . . 9  |-  suc  A  =  ( A  u.  { A } )
87eleq2i 2470 . . . . . . . 8  |-  ( x  e.  suc  A  <->  x  e.  ( A  u.  { A } ) )
9 elun 3572 . . . . . . . 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 512 . . . . . . 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 4882 . . . . . 6  |-  A  C_  suc  A
14 sstr2 3437 . . . . . 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 2804 . . . 4  |-  ( A  e.  On  ->  A. x  e.  suc  A x  C_  suc  A )
17 dftr3 4477 . . . 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 6543 . . . . 5  |-  ( A  e.  On  ->  A  C_  On )
20 snssi 4101 . . . . 5  |-  ( A  e.  On  ->  { A }  C_  On )
2119, 20unssd 3607 . . . 4  |-  ( A  e.  On  ->  ( A  u.  { A } )  C_  On )
227, 21syl5eqss 3474 . . 3  |-  ( A  e.  On  ->  suc  A 
C_  On )
23 ordon 6535 . . . 4  |-  Ord  On
24 trssord 4822 . . . . 5  |-  ( ( Tr  suc  A  /\  suc  A  C_  On  /\  Ord  On )  ->  Ord  suc  A
)
25243exp 1193 . . . 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 6562 . . 3  |-  ( A  e.  On  ->  suc  A  e.  _V )
29 elong 4813 . . 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 366    = wceq 1399    e. wcel 1836   A.wral 2742   _Vcvv 3047    u. cun 3400    C_ wss 3402   {csn 3957   Tr wtr 4473   Ord word 4804   Oncon0 4805   suc csuc 4807
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-sep 4501  ax-nul 4509  ax-pr 4614  ax-un 6509
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-ral 2747  df-rex 2748  df-rab 2751  df-v 3049  df-sbc 3266  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-pss 3418  df-nul 3725  df-if 3871  df-sn 3958  df-pr 3960  df-tp 3962  df-op 3964  df-uni 4177  df-br 4381  df-opab 4439  df-tr 4474  df-eprel 4718  df-po 4727  df-so 4728  df-fr 4765  df-we 4767  df-ord 4808  df-on 4809  df-suc 4811
This theorem is referenced by:  ordsuc  6566  unon  6583  onsuci  6590  ordunisuc2  6596  ordzsl  6597  onzsl  6598  tfindsg  6612  dfom2  6619  findsg  6644  tfrlem12  6994  oasuc  7110  omsuc  7112  onasuc  7114  oacl  7121  oneo  7166  omeulem1  7167  omeulem2  7168  oeordi  7172  oeworde  7178  oelim2  7180  oelimcl  7185  oeeulem  7186  oeeui  7187  oaabs2  7230  omxpenlem  7555  card2inf  7914  cantnflt  8022  cantnflem1d  8038  cantnfltOLD  8052  cantnflem1dOLD  8061  cnfcom  8075  cnfcomOLD  8083  r1ordg  8127  bndrank  8190  r1pw  8194  r1pwALT  8195  tcrank  8233  onssnum  8352  dfac12lem2  8455  cfsuc  8568  cfsmolem  8581  fin1a2lem1  8711  fin1a2lem2  8712  ttukeylem7  8826  alephreg  8888  gch2  8982  winainflem  9000  winalim2  9003  r1wunlim  9044  nqereu  9236  ontgval  30085  ontgsucval  30086  onsuctop  30087
  Copyright terms: Public domain W3C validator