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

Theorem trsuc 4971
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 4964 . . . . . 6  |-  B  C_  suc  B
2 ssexg 4602 . . . . . 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 4965 . . . . 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 4557 . . 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 1819   _Vcvv 3109    C_ wss 3471   Tr wtr 4550   suc csuc 4889
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3476  df-in 3478  df-ss 3485  df-sn 4033  df-uni 4252  df-tr 4551  df-suc 4893
This theorem is referenced by:  onuninsuci  6674  limsuc  6683  tz7.44-2  7091  cantnflt  8108  cantnfp1lem3  8116  cantnflem1b  8122  cantnflem1  8125  cantnfltOLD  8138  cantnfp1lem3OLD  8142  cantnflem1bOLD  8145  cantnflem1OLD  8148  cnfcom  8161  cnfcomOLD  8169  axdc3lem2  8848  inar1  9170  limsuc2  31148  bnj967  34104
  Copyright terms: Public domain W3C validator