Theorem ordtr 6332

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

Syntax hints:   → wi 4  Tr wtr 5206   E cep 5524   We wwe 5577  Ord word 6317

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 6321

This theorem is referenced by:  ordelss  6334  ordn2lp  6338  ordelord  6340  tz7.7  6344  ordelssne  6345  ordin  6348  ordtr1  6362  orduniss  6417  ontr  6429  dford5  7731  ordsuci  7755  ordunisuc  7776  limsuc  7793  trom  7819  dfrecs3  8306  tz7.44-2  8340  cantnflt  9585  cantnfp1lem3  9593  cantnflem1b  9599  cantnflem1  9602  cnfcom  9613  axdc3lem2  10365  inar1  10690  efgmnvl  19647  bnj967  35103  dford3  43337  limsuc2  43350  ordsssucim  43711  ordelordALT  44845  onfrALTlem2  44854  ordelordALTVD  45174  onfrALTlem2VD  45196  iunord  49988