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

Theorem suceloni 4734
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 4565 . . . . . . . 8  |-  ( A  e.  On  ->  (
x  e.  A  ->  x  C_  A ) )
2 elsn 3773 . . . . . . . . . 10  |-  ( x  e.  { A }  <->  x  =  A )
3 eqimss 3344 . . . . . . . . . 10  |-  ( x  =  A  ->  x  C_  A )
42, 3sylbi 188 . . . . . . . . 9  |-  ( x  e.  { A }  ->  x  C_  A )
54a1i 11 . . . . . . . 8  |-  ( A  e.  On  ->  (
x  e.  { A }  ->  x  C_  A
) )
61, 5orim12d 812 . . . . . . 7  |-  ( A  e.  On  ->  (
( x  e.  A  \/  x  e.  { A } )  ->  (
x  C_  A  \/  x  C_  A ) ) )
7 df-suc 4529 . . . . . . . . 9  |-  suc  A  =  ( A  u.  { A } )
87eleq2i 2452 . . . . . . . 8  |-  ( x  e.  suc  A  <->  x  e.  ( A  u.  { A } ) )
9 elun 3432 . . . . . . . 8  |-  ( x  e.  ( A  u.  { A } )  <->  ( x  e.  A  \/  x  e.  { A } ) )
108, 9bitr2i 242 . . . . . . 7  |-  ( ( x  e.  A  \/  x  e.  { A } )  <->  x  e.  suc  A )
11 oridm 501 . . . . . . 7  |-  ( ( x  C_  A  \/  x  C_  A )  <->  x  C_  A
)
126, 10, 113imtr3g 261 . . . . . 6  |-  ( A  e.  On  ->  (
x  e.  suc  A  ->  x  C_  A )
)
13 sssucid 4600 . . . . . 6  |-  A  C_  suc  A
14 sstr2 3299 . . . . . 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 2732 . . . 4  |-  ( A  e.  On  ->  A. x  e.  suc  A x  C_  suc  A )
17 dftr3 4248 . . . 4  |-  ( Tr 
suc  A  <->  A. x  e.  suc  A x  C_  suc  A )
1816, 17sylibr 204 . . 3  |-  ( A  e.  On  ->  Tr  suc  A )
19 onss 4712 . . . . 5  |-  ( A  e.  On  ->  A  C_  On )
20 snssi 3886 . . . . 5  |-  ( A  e.  On  ->  { A }  C_  On )
2119, 20unssd 3467 . . . 4  |-  ( A  e.  On  ->  ( A  u.  { A } )  C_  On )
227, 21syl5eqss 3336 . . 3  |-  ( A  e.  On  ->  suc  A 
C_  On )
23 ordon 4704 . . . 4  |-  Ord  On
24 trssord 4540 . . . . 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 4731 . . 3  |-  ( A  e.  On  ->  suc  A  e.  _V )
29 elong 4531 . . 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 224 1  |-  ( A  e.  On  ->  suc  A  e.  On )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    \/ wo 358    = wceq 1649    e. wcel 1717   A.wral 2650   _Vcvv 2900    u. cun 3262    C_ wss 3264   {csn 3758   Tr wtr 4244   Ord word 4522   Oncon0 4523   suc csuc 4525
This theorem is referenced by:  ordsuc  4735  unon  4752  onsuci  4759  ordunisuc2  4765  ordzsl  4766  onzsl  4767  tfindsg  4781  dfom2  4788  findsg  4813  tfrlem12  6587  oasuc  6705  omsuc  6707  onasuc  6709  oacl  6716  oneo  6761  omeulem1  6762  omeulem2  6763  oeordi  6767  oeworde  6773  oelim2  6775  oelimcl  6780  oeeulem  6781  oeeui  6782  oaabs2  6825  omxpenlem  7146  card2inf  7457  cantnflt  7561  cantnflem1d  7578  cnfcom  7591  r1ordg  7638  bndrank  7701  r1pw  7705  r1pwOLD  7706  tcrank  7742  onssnum  7855  dfac12lem2  7958  cfsuc  8071  cfsmolem  8084  fin1a2lem1  8214  fin1a2lem2  8215  ttukeylem7  8329  alephreg  8391  gch2  8488  winainflem  8502  winalim2  8505  r1wunlim  8546  nqereu  8740  ontgval  25896  ontgsucval  25897  onsuctop  25898
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369  ax-sep 4272  ax-nul 4280  ax-pr 4345  ax-un 4642
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2243  df-mo 2244  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-ne 2553  df-ral 2655  df-rex 2656  df-rab 2659  df-v 2902  df-sbc 3106  df-dif 3267  df-un 3269  df-in 3271  df-ss 3278  df-pss 3280  df-nul 3573  df-if 3684  df-sn 3764  df-pr 3765  df-tp 3766  df-op 3767  df-uni 3959  df-br 4155  df-opab 4209  df-tr 4245  df-eprel 4436  df-po 4445  df-so 4446  df-fr 4483  df-we 4485  df-ord 4526  df-on 4527  df-suc 4529
  Copyright terms: Public domain W3C validator