Theorem ordtr 6328

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

Syntax hints:   → wi 4  Tr wtr 5182   E cep 5520   We wwe 5573  Ord word 6313

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 398  df-ord 6317

This theorem is referenced by:  ordelss  6330  ordn2lp  6334  ordelord  6336  tz7.7  6340  ordelssne  6341  ordin  6344  ordtr1  6358  orduniss  6413  ontr  6425  dford5  7731  ordsuci  7755  ordunisuc  7776  limsuc  7793  trom  7819  dfrecs3  8306  tz7.44-2  8340  cantnflt  9588  cantnfp1lem3  9596  cantnflem1b  9602  cantnflem1  9605  cnfcom  9616  axdc3lem2  10368  inar1  10693  efgmnvl  19684  bnj967  35142  dford3  43488  limsuc2  43501  ordsssucim  43862  ordelordALT  44996  onfrALTlem2  45005  ordelordALTVD  45325  onfrALTlem2VD  45347  iunord  50180