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

Theorem ordtr 6198
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 6187 . 2 (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
21simplbi 498 1 (Ord 𝐴 → Tr 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Tr wtr 5163   E cep 5457   We wwe 5506  Ord word 6183
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 208  df-an 397  df-ord 6187
This theorem is referenced by:  ordelss  6200  ordn2lp  6204  ordelord  6206  tz7.7  6210  ordelssne  6211  ordin  6214  ordtr1  6227  orduniss  6278  ontrci  6289  ordunisuc  7536  onuninsuci  7544  limsuc  7553  ordom  7578  elnn  7579  omsinds  7589  dfrecs3  7998  tz7.44-2  8032  cantnflt  9123  cantnfp1lem3  9131  cantnflem1b  9137  cantnflem1  9140  cnfcom  9151  axdc3lem2  9861  inar1  10185  efgmnvl  18769  bnj967  32116  dford5  32854  dford3  39503  limsuc2  39519  ordelordALT  40748  onfrALTlem2  40757  ordelordALTVD  41078  onfrALTlem2VD  41100  iunord  44707
  Copyright terms: Public domain W3C validator