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

Theorem ordtr 4597
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 4586 . 2  |-  ( Ord 
A  <->  ( Tr  A  /\  _E  We  A ) )
21simplbi 448 1  |-  ( Ord 
A  ->  Tr  A
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   Tr wtr 4304    _E cep 4494    We wwe 4542   Ord word 4582
This theorem is referenced by:  ordelss  4599  ordn2lp  4603  ordelord  4605  tz7.7  4609  ordelssne  4610  ordin  4613  ordtr1  4626  orduniss  4678  ontrci  4689  ordunisuc  4814  onuninsuci  4822  limsuc  4831  ordom  4856  elnn  4857  tz7.44-2  6667  cantnflt  7629  cantnfp1lem3  7638  cantnflem1b  7644  cantnflem1  7647  cnfcom  7659  axdc3lem2  8333  inar1  8652  efgmnvl  15348  omsinds  25496  dford3  27101  limsuc2  27117  ordelordALT  28684  onfrALTlem2  28694  ordelordALTVD  29041  onfrALTlem2VD  29063  bnj967  29378
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 179  df-an 362  df-ord 4586
  Copyright terms: Public domain W3C validator