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

Theorem ordtr 4897
 Description: An ordinal class is transitive. (Contributed by NM, 3-Apr-1994.)
Assertion
Ref Expression
ordtr

Proof of Theorem ordtr
StepHypRef Expression
1 df-ord 4886 . 2
21simplbi 460 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  Trwtr 4545   cep 4794  Wewwe 4842  Ordword 4882 This theorem is referenced by:  ordelss  4899  ordn2lp  4903  ordelord  4905  tz7.7  4909  ordelssne  4910  ordin  4913  ordtr1  4926  orduniss  4977  ontrci  4988  ordunisuc  6667  onuninsuci  6675  limsuc  6684  ordom  6709  elnn  6710  tz7.44-2  7092  cantnflt  8112  cantnfp1lem3  8120  cantnflem1b  8126  cantnflem1  8129  cantnfltOLD  8142  cantnfp1lem3OLD  8146  cantnflem1bOLD  8149  cantnflem1OLD  8152  cnfcom  8165  cnfcomOLD  8173  axdc3lem2  8852  inar1  9174  efgmnvl  16732  omsinds  29299  dford3  30970  limsuc2  30986  ordelordALT  33308  onfrALTlem2  33318  ordelordALTVD  33667  onfrALTlem2VD  33689  bnj967  34003 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 4886
 Copyright terms: Public domain W3C validator