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

Theorem ordtr 5701
Description: An ordinal class is transitive. (Contributed by NM, 3-Apr-1994.)
Assertion
Ref Expression
ordtr (Ord 𝐴 → Tr 𝐴)

Proof of Theorem ordtr
StepHypRef Expression
1 df-ord 5690 . 2 (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
21simplbi 476 1 (Ord 𝐴 → Tr 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Tr wtr 4717   E cep 4988   We wwe 5037  Ord word 5686
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 197  df-an 386  df-ord 5690
This theorem is referenced by:  ordelss  5703  ordn2lp  5707  ordelord  5709  tz7.7  5713  ordelssne  5714  ordin  5717  ordtr1  5731  orduniss  5785  ontrci  5797  ordunisuc  6986  onuninsuci  6994  limsuc  7003  ordom  7028  elnn  7029  omsinds  7038  dfrecs3  7421  tz7.44-2  7455  cantnflt  8521  cantnfp1lem3  8529  cantnflem1b  8535  cantnflem1  8538  cnfcom  8549  axdc3lem2  9225  inar1  9549  efgmnvl  18059  bnj967  30758  dford5  31352  dford3  37110  limsuc2  37126  ordelordALT  38264  onfrALTlem2  38278  ordelordALTVD  38621  onfrALTlem2VD  38643  iunord  41740
  Copyright terms: Public domain W3C validator