Theorem ordtr 6362

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

Syntax hints:   → wi 4  Tr wtr 5209   E cep 5548   We wwe 5601  Ord word 6347

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 400  df-ord 6351

This theorem is referenced by:  ordelss  6364  ordn2lp  6368  ordelord  6370  tz7.7  6374  ordelssne  6375  ordin  6378  ordtr1  6392  orduniss  6447  ontr  6459  dford5  7769  ordsuci  7793  ordunisuc  7814  limsuc  7831  trom  7857  dfrecs3  8345  tz7.44-2  8380  cantnflt  9629  cantnfp1lem3  9637  cantnflem1b  9643  cantnflem1  9646  cnfcom  9657  axdc3lem2  10410  inar1  10735  efgmnvl  19756  bnj967  35242  dford3  43610  limsuc2  43623  ordsssucim  43984  ordelordALT  45118  onfrALTlem2  45127  ordelordALTVD  45447  onfrALTlem2VD  45469  iunord  50302