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

Theorem ordtr 5775
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 5764 . 2 (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
21simplbi 475 1 (Ord 𝐴 → Tr 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Tr wtr 4785   E cep 5057   We wwe 5101  Ord word 5760
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 385  df-ord 5764
This theorem is referenced by:  ordelss  5777  ordn2lp  5781  ordelord  5783  tz7.7  5787  ordelssne  5788  ordin  5791  ordtr1  5805  orduniss  5859  ontrci  5871  ordunisuc  7074  onuninsuci  7082  limsuc  7091  ordom  7116  elnn  7117  omsinds  7126  dfrecs3  7514  tz7.44-2  7548  cantnflt  8607  cantnfp1lem3  8615  cantnflem1b  8621  cantnflem1  8624  cnfcom  8635  axdc3lem2  9311  inar1  9635  efgmnvl  18173  bnj967  31141  dford5  31734  dford3  37912  limsuc2  37928  ordelordALT  39064  onfrALTlem2  39078  ordelordALTVD  39417  onfrALTlem2VD  39439  iunord  42747
  Copyright terms: Public domain W3C validator