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

Theorem ordtr 4898
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 4887 . 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 4546    _E cep 4795    We wwe 4843   Ord word 4883
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 4887
This theorem is referenced by:  ordelss  4900  ordn2lp  4904  ordelord  4906  tz7.7  4910  ordelssne  4911  ordin  4914  ordtr1  4927  orduniss  4978  ontrci  4989  ordunisuc  6662  onuninsuci  6670  limsuc  6679  ordom  6704  elnn  6705  tz7.44-2  7085  cantnflt  8103  cantnfp1lem3  8111  cantnflem1b  8117  cantnflem1  8120  cantnfltOLD  8133  cantnfp1lem3OLD  8137  cantnflem1bOLD  8140  cantnflem1OLD  8143  cnfcom  8156  cnfcomOLD  8164  axdc3lem2  8843  inar1  9165  efgmnvl  16605  omsinds  29226  dford3  30898  limsuc2  30914  ordelordALT  32789  onfrALTlem2  32799  ordelordALTVD  33148  onfrALTlem2VD  33170  bnj967  33483
  Copyright terms: Public domain W3C validator