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

Theorem ordtr 4422
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 4411 . 2  |-  ( Ord 
A  <->  ( Tr  A  /\  _E  We  A ) )
21simplbi 446 1  |-  ( Ord 
A  ->  Tr  A
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   Tr wtr 4129    _E cep 4319    We wwe 4367   Ord word 4407
This theorem is referenced by:  ordelss  4424  ordn2lp  4428  ordelord  4430  tz7.7  4434  ordelssne  4435  ordin  4438  ordtr1  4451  orduniss  4503  ontrci  4514  ordunisuc  4639  onuninsuci  4647  limsuc  4656  ordom  4681  elnn  4682  tz7.44-2  6436  cantnflt  7389  cantnfp1lem3  7398  cantnflem1b  7404  cantnflem1  7407  cnfcom  7419  axdc3lem2  8093  inar1  8413  efgmnvl  15039  omsinds  24290  imresord  25202  ordsuccl  25205  ordsuccl2  25206  ordsuccl3  25207  tartarmap  25991  eltintpar  26002  inttaror  26003  dford3  27224  limsuc2  27240  ordelordALT  28600  onfrALTlem2  28610  ordelordALTVD  28959  onfrALTlem2VD  28981  bnj967  29293
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 177  df-an 360  df-ord 4411
  Copyright terms: Public domain W3C validator