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

Theorem ordtr 5955
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 5944 . 2 (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
21simplbi 492 1 (Ord 𝐴 → Tr 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Tr wtr 4945   E cep 5224   We wwe 5270  Ord word 5940
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 199  df-an 386  df-ord 5944
This theorem is referenced by:  ordelss  5957  ordn2lp  5961  ordelord  5963  tz7.7  5967  ordelssne  5968  ordin  5971  ordtr1  5984  orduniss  6035  ontrci  6046  ordunisuc  7266  onuninsuci  7274  limsuc  7283  ordom  7308  elnn  7309  omsinds  7318  dfrecs3  7708  tz7.44-2  7742  cantnflt  8819  cantnfp1lem3  8827  cantnflem1b  8833  cantnflem1  8836  cnfcom  8847  axdc3lem2  9561  inar1  9885  efgmnvl  18440  bnj967  31532  dford5  32123  dford3  38376  limsuc2  38392  ordelordALT  39519  onfrALTlem2  39528  ordelordALTVD  39859  onfrALTlem2VD  39881  iunord  43217
  Copyright terms: Public domain W3C validator