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

Theorem trsuc 4968
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 4961 . . . . . 6  |-  B  C_  suc  B
2 ssexg 4599 . . . . . 6  |-  ( ( B  C_  suc  B  /\  suc  B  e.  A )  ->  B  e.  _V )
31, 2mpan 670 . . . . 5  |-  ( suc 
B  e.  A  ->  B  e.  _V )
4 sucidg 4962 . . . . 5  |-  ( B  e.  _V  ->  B  e.  suc  B )
53, 4syl 16 . . . 4  |-  ( suc 
B  e.  A  ->  B  e.  suc  B )
65ancri 552 . . 3  |-  ( suc 
B  e.  A  -> 
( B  e.  suc  B  /\  suc  B  e.  A ) )
7 trel 4553 . . 3  |-  ( Tr  A  ->  ( ( B  e.  suc  B  /\  suc  B  e.  A )  ->  B  e.  A
) )
86, 7syl5 32 . 2  |-  ( Tr  A  ->  ( suc  B  e.  A  ->  B  e.  A ) )
98imp 429 1  |-  ( ( Tr  A  /\  suc  B  e.  A )  ->  B  e.  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1767   _Vcvv 3118    C_ wss 3481   Tr wtr 4546   suc csuc 4886
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4574
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3120  df-un 3486  df-in 3488  df-ss 3495  df-sn 4034  df-uni 4252  df-tr 4547  df-suc 4890
This theorem is referenced by:  onuninsuci  6670  limsuc  6679  tz7.44-2  7085  cantnflt  8103  cantnfp1lem3  8111  cantnflem1b  8117  cantnflem1  8120  cantnfltOLD  8133  cantnfp1lem3OLD  8137  cantnflem1bOLD  8140  cantnflem1OLD  8143  cnfcom  8156  cnfcomOLD  8164  axdc3lem2  8843  inar1  9165  limsuc2  30914  bnj967  33483
  Copyright terms: Public domain W3C validator