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

Theorem ordtr 6202
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 6191 . 2 (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
21simplbi 498 1 (Ord 𝐴 → Tr 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Tr wtr 5168   E cep 5462   We wwe 5511  Ord word 6187
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 6191
This theorem is referenced by:  ordelss  6204  ordn2lp  6208  ordelord  6210  tz7.7  6214  ordelssne  6215  ordin  6218  ordtr1  6231  orduniss  6282  ontrci  6293  ordunisuc  7538  onuninsuci  7546  limsuc  7555  ordom  7580  elnn  7581  omsinds  7591  dfrecs3  8003  tz7.44-2  8037  cantnflt  9127  cantnfp1lem3  9135  cantnflem1b  9141  cantnflem1  9144  cnfcom  9155  axdc3lem2  9865  inar1  10189  efgmnvl  18762  bnj967  32103  dford5  32841  dford3  39486  limsuc2  39502  ordelordALT  40732  onfrALTlem2  40741  ordelordALTVD  41062  onfrALTlem2VD  41084  iunord  44607
  Copyright terms: Public domain W3C validator