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

Theorem ordtr 5654
 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 5643 . 2 (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
21simplbi 475 1 (Ord 𝐴 → Tr 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  Tr wtr 4680   E cep 4947   We wwe 4996  Ord word 5639 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 196  df-an 385  df-ord 5643 This theorem is referenced by:  ordelss  5656  ordn2lp  5660  ordelord  5662  tz7.7  5666  ordelssne  5667  ordin  5670  ordtr1  5684  orduniss  5738  ontrci  5750  ordunisuc  6924  onuninsuci  6932  limsuc  6941  ordom  6966  elnn  6967  omsinds  6976  dfrecs3  7356  tz7.44-2  7390  cantnflt  8452  cantnfp1lem3  8460  cantnflem1b  8466  cantnflem1  8469  cnfcom  8480  axdc3lem2  9156  inar1  9476  efgmnvl  17950  bnj967  30269  dford3  36613  limsuc2  36629  ordelordALT  37768  onfrALTlem2  37782  ordelordALTVD  38125  onfrALTlem2VD  38147  iunord  42220
 Copyright terms: Public domain W3C validator