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

Theorem ordtr 5456
Description: An ordinal class is transitive. (Contributed by NM, 3-Apr-1994.)
Assertion
Ref Expression
ordtr  |-  ( Ord 
A  ->  Tr  A
)

Proof of Theorem ordtr
StepHypRef Expression
1 df-ord 5445 . 2  |-  ( Ord 
A  <->  ( Tr  A  /\  _E  We  A ) )
21simplbi 461 1  |-  ( Ord 
A  ->  Tr  A
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   Tr wtr 4518    _E cep 4762    We wwe 4811   Ord word 5441
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 188  df-an 372  df-ord 5445
This theorem is referenced by:  ordelss  5458  ordn2lp  5462  ordelord  5464  tz7.7  5468  ordelssne  5469  ordin  5472  ordtr1  5485  orduniss  5536  ontrci  5547  ordunisuc  6673  onuninsuci  6681  limsuc  6690  ordom  6715  elnn  6716  omsinds  6725  dfrecs3  7102  tz7.44-2  7136  cantnflt  8185  cantnfp1lem3  8193  cantnflem1b  8199  cantnflem1  8202  cnfcom  8213  axdc3lem2  8888  inar1  9207  efgmnvl  17363  bnj967  29764  dford3  35853  limsuc2  35869  ordelordALT  36868  onfrALTlem2  36882  ordelordALTVD  37237  onfrALTlem2VD  37259
  Copyright terms: Public domain W3C validator