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

Theorem trsuc 4914
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 4907 . . . . . 6  |-  B  C_  suc  B
2 ssexg 4549 . . . . . 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 4908 . . . . 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 4503 . . 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 1758   _Vcvv 3078    C_ wss 3439   Tr wtr 4496   suc csuc 4832
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4524
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3080  df-un 3444  df-in 3446  df-ss 3453  df-sn 3989  df-uni 4203  df-tr 4497  df-suc 4836
This theorem is referenced by:  onuninsuci  6564  limsuc  6573  tz7.44-2  6976  cantnflt  7995  cantnfp1lem3  8003  cantnflem1b  8009  cantnflem1  8012  cantnfltOLD  8025  cantnfp1lem3OLD  8029  cantnflem1bOLD  8032  cantnflem1OLD  8035  cnfcom  8048  cnfcomOLD  8056  axdc3lem2  8735  inar1  9057  limsuc2  29564  bnj967  32293
  Copyright terms: Public domain W3C validator