Theorem ordtr 5880

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

Syntax hints:   → wi 4  Tr wtr 4886   E cep 5161   We wwe 5207  Ord word 5865

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 197  df-an 383  df-ord 5869

This theorem is referenced by:  ordelss  5882  ordn2lp  5886  ordelord  5888  tz7.7  5892  ordelssne  5893  ordin  5896  ordtr1  5910  orduniss  5964  ontrci  5976  ordunisuc  7179  onuninsuci  7187  limsuc  7196  ordom  7221  elnn  7222  omsinds  7231  dfrecs3  7622  tz7.44-2  7656  cantnflt  8733  cantnfp1lem3  8741  cantnflem1b  8747  cantnflem1  8750  cnfcom  8761  axdc3lem2  9475  inar1  9799  efgmnvl  18334  bnj967  31353  dford5  31946  dford3  38121  limsuc2  38137  ordelordALT  39272  onfrALTlem2  39286  ordelordALTVD  39625  onfrALTlem2VD  39647  iunord  42950