Theorem ordtr 6346

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

Syntax hints:   → wi 4  Tr wtr 5214   E cep 5537   We wwe 5590  Ord word 6331

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 6335

This theorem is referenced by:  ordelss  6348  ordn2lp  6352  ordelord  6354  tz7.7  6358  ordelssne  6359  ordin  6362  ordtr1  6376  orduniss  6431  ontr  6443  dford5  7760  ordsuci  7784  ordunisuc  7807  limsuc  7825  trom  7851  dfrecs3  8341  tz7.44-2  8375  cantnflt  9625  cantnfp1lem3  9633  cantnflem1b  9639  cantnflem1  9642  cnfcom  9653  axdc3lem2  10404  inar1  10728  efgmnvl  19644  bnj967  34935  dford3  43017  limsuc2  43030  ordsssucim  43391  ordelordALT  44527  onfrALTlem2  44536  ordelordALTVD  44856  onfrALTlem2VD  44878  iunord  49665