Theorem ordtr 6199

Description: An ordinal class is transitive. (Contributed by NM, 3-Apr-1994.)

Assertion

Ref	Expression
ordtr	⊢ (Ord 𝐴 → Tr 𝐴)

Proof of Theorem ordtr

Step	Hyp	Ref	Expression
1		df-ord 6188	. 2 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
2	1	simplbi 500	1 ⊢ (Ord 𝐴 → Tr 𝐴)

Syntax hints:   → wi 4  Tr wtr 5164   E cep 5458   We wwe 5507  Ord word 6184

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 209  df-an 399  df-ord 6188

This theorem is referenced by:  ordelss  6201  ordn2lp  6205  ordelord  6207  tz7.7  6211  ordelssne  6212  ordin  6215  ordtr1  6228  orduniss  6279  ontrci  6290  ordunisuc  7541  onuninsuci  7549  limsuc  7558  ordom  7583  elnn  7584  omsinds  7594  dfrecs3  8003  tz7.44-2  8037  cantnflt  9129  cantnfp1lem3  9137  cantnflem1b  9143  cantnflem1  9146  cnfcom  9157  axdc3lem2  9867  inar1  10191  efgmnvl  18834  bnj967  32212  dford5  32952  dford3  39618  limsuc2  39634  ordelordALT  40864  onfrALTlem2  40873  ordelordALTVD  41194  onfrALTlem2VD  41216  iunord  44773