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

Theorem trsuc 4476
Description: A set whose successor belongs to a transitive class also belongs. (Contributed by NM, 5-Sep-2003.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
Assertion
Ref Expression
trsuc  |-  ( ( Tr  A  /\  suc  B  e.  A )  ->  B  e.  A )

Proof of Theorem trsuc
StepHypRef Expression
1 sssucid 4469 . . . . . 6  |-  B  C_  suc  B
2 ssexg 4160 . . . . . 6  |-  ( ( B  C_  suc  B  /\  suc  B  e.  A )  ->  B  e.  _V )
31, 2mpan 651 . . . . 5  |-  ( suc 
B  e.  A  ->  B  e.  _V )
4 sucidg 4470 . . . . 5  |-  ( B  e.  _V  ->  B  e.  suc  B )
53, 4syl 15 . . . 4  |-  ( suc 
B  e.  A  ->  B  e.  suc  B )
65ancri 535 . . 3  |-  ( suc 
B  e.  A  -> 
( B  e.  suc  B  /\  suc  B  e.  A ) )
7 trel 4120 . . 3  |-  ( Tr  A  ->  ( ( B  e.  suc  B  /\  suc  B  e.  A )  ->  B  e.  A
) )
86, 7syl5 28 . 2  |-  ( Tr  A  ->  ( suc  B  e.  A  ->  B  e.  A ) )
98imp 418 1  |-  ( ( Tr  A  /\  suc  B  e.  A )  ->  B  e.  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1684   _Vcvv 2788    C_ wss 3152   Tr wtr 4113   suc csuc 4394
This theorem is referenced by:  onuninsuci  4631  limsuc  4640  tz7.44-2  6420  cantnflt  7373  cantnfp1lem3  7382  cantnflem1b  7388  cantnflem1  7391  cnfcom  7403  axdc3lem2  8077  inar1  8397  ordsuccl  25102  ordsuccl2  25103  tartarmap  25888  limsuc2  27137  bnj967  28977
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157  df-in 3159  df-ss 3166  df-sn 3646  df-uni 3828  df-tr 4114  df-suc 4398
  Copyright terms: Public domain W3C validator