Theorem ordtr 6400

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

Syntax hints:   → wi 4  Tr wtr 5265   E cep 5588   We wwe 5640  Ord word 6385

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 6389

This theorem is referenced by:  ordelss  6402  ordn2lp  6406  ordelord  6408  tz7.7  6412  ordelssne  6413  ordin  6416  ordtr1  6429  orduniss  6483  ontr  6495  dford5  7803  ordsuci  7828  ordunisuc  7852  limsuc  7870  trom  7896  omsindsOLD  7909  dfrecs3  8411  dfrecs3OLD  8412  tz7.44-2  8446  cantnflt  9710  cantnfp1lem3  9718  cantnflem1b  9724  cantnflem1  9727  cnfcom  9738  axdc3lem2  10489  inar1  10813  efgmnvl  19747  bnj967  34938  dford3  43017  limsuc2  43030  ordsssucim  43392  ordelordALT  44535  onfrALTlem2  44544  ordelordALTVD  44865  onfrALTlem2VD  44887  iunord  48907