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

Theorem ordtr 5880
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 5869 . 2 (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
21simplbi 479 1 (Ord 𝐴 → Tr 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Tr wtr 4886   E cep 5161   We wwe 5207  Ord word 5865
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 197  df-an 383  df-ord 5869
This theorem is referenced by:  ordelss  5882  ordn2lp  5886  ordelord  5888  tz7.7  5892  ordelssne  5893  ordin  5896  ordtr1  5910  orduniss  5964  ontrci  5976  ordunisuc  7179  onuninsuci  7187  limsuc  7196  ordom  7221  elnn  7222  omsinds  7231  dfrecs3  7622  tz7.44-2  7656  cantnflt  8733  cantnfp1lem3  8741  cantnflem1b  8747  cantnflem1  8750  cnfcom  8761  axdc3lem2  9475  inar1  9799  efgmnvl  18334  bnj967  31353  dford5  31946  dford3  38121  limsuc2  38137  ordelordALT  39272  onfrALTlem2  39286  ordelordALTVD  39625  onfrALTlem2VD  39647  iunord  42950
  Copyright terms: Public domain W3C validator