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

Theorem ordtr 6398
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 6387 . 2 (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
21simplbi 497 1 (Ord 𝐴 → Tr 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Tr wtr 5259   E cep 5583   We wwe 5636  Ord word 6383
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 207  df-an 396  df-ord 6387
This theorem is referenced by:  ordelss  6400  ordn2lp  6404  ordelord  6406  tz7.7  6410  ordelssne  6411  ordin  6414  ordtr1  6427  orduniss  6481  ontr  6493  dford5  7804  ordsuci  7828  ordunisuc  7852  limsuc  7870  trom  7896  dfrecs3  8412  dfrecs3OLD  8413  tz7.44-2  8447  cantnflt  9712  cantnfp1lem3  9720  cantnflem1b  9726  cantnflem1  9729  cnfcom  9740  axdc3lem2  10491  inar1  10815  efgmnvl  19732  bnj967  34959  dford3  43040  limsuc2  43053  ordsssucim  43415  ordelordALT  44557  onfrALTlem2  44566  ordelordALTVD  44887  onfrALTlem2VD  44909  iunord  49195
  Copyright terms: Public domain W3C validator