Theorem ordtr 6409

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 6398	. 2 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
2	1	simplbi 497	1 ⊢ (Ord 𝐴 → Tr 𝐴)

Syntax hints:   → wi 4  Tr wtr 5283   E cep 5598   We wwe 5651  Ord word 6394

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 207  df-an 396  df-ord 6398

This theorem is referenced by:  ordelss  6411  ordn2lp  6415  ordelord  6417  tz7.7  6421  ordelssne  6422  ordin  6425  ordtr1  6438  orduniss  6492  ontr  6504  dford5  7819  ordsuci  7844  ordunisuc  7868  limsuc  7886  trom  7912  omsindsOLD  7925  dfrecs3  8428  dfrecs3OLD  8429  tz7.44-2  8463  cantnflt  9741  cantnfp1lem3  9749  cantnflem1b  9755  cantnflem1  9758  cnfcom  9769  axdc3lem2  10520  inar1  10844  efgmnvl  19756  bnj967  34921  dford3  42985  limsuc2  42998  ordsssucim  43364  ordelordALT  44508  onfrALTlem2  44517  ordelordALTVD  44838  onfrALTlem2VD  44860  iunord  48768