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

Theorem ordtr 4406
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 4395 . 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 4113    _E cep 4303    We wwe 4351   Ord word 4391
This theorem is referenced by:  ordelss  4408  ordn2lp  4412  ordelord  4414  tz7.7  4418  ordelssne  4419  ordin  4422  ordtr1  4435  orduniss  4487  ontrci  4498  ordunisuc  4623  onuninsuci  4631  limsuc  4640  ordom  4665  elnn  4666  tz7.44-2  6420  cantnflt  7373  cantnfp1lem3  7382  cantnflem1b  7388  cantnflem1  7391  cnfcom  7403  axdc3lem2  8077  inar1  8397  efgmnvl  15023  omsinds  24219  imresord  25099  ordsuccl  25102  ordsuccl2  25103  ordsuccl3  25104  tartarmap  25888  eltintpar  25899  inttaror  25900  dford3  27121  limsuc2  27137  ordelordALT  28301  onfrALTlem2  28311  ordelordALTVD  28643  onfrALTlem2VD  28665  bnj967  28977
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 4395
  Copyright terms: Public domain W3C validator