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

Theorem ordtr 5426
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 5415 . 2  |-  ( Ord 
A  <->  ( Tr  A  /\  _E  We  A ) )
21simplbi 460 1  |-  ( Ord 
A  ->  Tr  A
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   Tr wtr 4491    _E cep 4734    We wwe 4783   Ord word 5411
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 187  df-an 371  df-ord 5415
This theorem is referenced by:  ordelss  5428  ordn2lp  5432  ordelord  5434  tz7.7  5438  ordelssne  5439  ordin  5442  ordtr1  5455  orduniss  5506  ontrci  5517  ordunisuc  6652  onuninsuci  6660  limsuc  6669  ordom  6694  elnn  6695  omsinds  6704  dfrecs3  7078  tz7.44-2  7112  cantnflt  8125  cantnfp1lem3  8133  cantnflem1b  8139  cantnflem1  8142  cantnfltOLD  8155  cantnfp1lem3OLD  8159  cantnflem1bOLD  8162  cantnflem1OLD  8165  cnfcom  8178  cnfcomOLD  8186  axdc3lem2  8865  inar1  9185  efgmnvl  17058  bnj967  29343  dford3  35345  limsuc2  35361  ordelordALT  36341  onfrALTlem2  36355  ordelordALTVD  36711  onfrALTlem2VD  36733
  Copyright terms: Public domain W3C validator