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

Theorem ordtr 4844
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 4833 . 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 4496    _E cep 4741    We wwe 4789   Ord word 4829
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 185  df-an 371  df-ord 4833
This theorem is referenced by:  ordelss  4846  ordn2lp  4850  ordelord  4852  tz7.7  4856  ordelssne  4857  ordin  4860  ordtr1  4873  orduniss  4924  ontrci  4935  ordunisuc  6556  onuninsuci  6564  limsuc  6573  ordom  6598  elnn  6599  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  efgmnvl  16336  omsinds  27847  dford3  29548  limsuc2  29564  ordelordALT  31599  onfrALTlem2  31609  ordelordALTVD  31958  onfrALTlem2VD  31980  bnj967  32293
  Copyright terms: Public domain W3C validator