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

Theorem ordtr 6188
 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 6177 . 2 (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
21simplbi 501 1 (Ord 𝐴 → Tr 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  Tr wtr 5142   E cep 5438   We wwe 5486  Ord word 6173 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 210  df-an 400  df-ord 6177 This theorem is referenced by:  ordelss  6190  ordn2lp  6194  ordelord  6196  tz7.7  6200  ordelssne  6201  ordin  6204  ordtr1  6217  orduniss  6268  ontrci  6280  ordunisuc  7552  onuninsuci  7560  limsuc  7569  ordom  7594  elnn  7595  omsinds  7605  dfrecs3  8025  tz7.44-2  8059  cantnflt  9181  cantnfp1lem3  9189  cantnflem1b  9195  cantnflem1  9198  cnfcom  9209  axdc3lem2  9924  inar1  10248  efgmnvl  18920  bnj967  32457  dford5  33201  dford3  40377  limsuc2  40393  ordelordALT  41651  onfrALTlem2  41660  ordelordALTVD  41981  onfrALTlem2VD  42003  iunord  45691
 Copyright terms: Public domain W3C validator