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

Theorem ordtr 5416
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 5405 . 2  |-  ( Ord 
A  <->  ( Tr  A  /\  _E  We  A ) )
21simplbi 466 1  |-  ( Ord 
A  ->  Tr  A
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   Tr wtr 4469    _E cep 4721    We wwe 4770   Ord word 5401
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 190  df-an 377  df-ord 5405
This theorem is referenced by:  ordelss  5418  ordn2lp  5422  ordelord  5424  tz7.7  5428  ordelssne  5429  ordin  5432  ordtr1  5445  orduniss  5496  ontrci  5507  ordunisuc  6647  onuninsuci  6655  limsuc  6664  ordom  6689  elnn  6690  omsinds  6699  dfrecs3  7078  tz7.44-2  7112  cantnflt  8164  cantnfp1lem3  8172  cantnflem1b  8178  cantnflem1  8181  cnfcom  8192  axdc3lem2  8868  inar1  9187  efgmnvl  17375  bnj967  29762  dford3  35885  limsuc2  35901  ordelordALT  36899  onfrALTlem2  36913  ordelordALTVD  37261  onfrALTlem2VD  37283
  Copyright terms: Public domain W3C validator