Theorem ordtr 6374

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

This proof depends on syntax axioms:   → wi 4  Tr wtr 5218   E cep 5560   We wwe 5613  Ord word 6359

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401  df-ord 6363

This theorem is used by:  ordelss  6376  ordn2lp  6380  ordelord  6382  tz7.7  6386  ordelssne  6387  ordin  6391  ordtr1  6405  orduniss  6460  ontr  6472  dford5  7779  ordsuci  7803  ordunisuc  7824  limsuc  7841  trom  7867  dfrecs3  8355  tz7.44-2  8390  cantnflt  9637  cantnfp1lem3  9645  cantnflem1b  9651  cantnflem1  9654  cnfcom  9665  axdc3lem2  10439  inar1  10764  efgmnvl  19788  bnj967  35342  dford3  43783  limsuc2  43796  ordsssucim  44157  ordelordALT  45274  onfrALTlem2  45283  ordelordALTVD  45603  onfrALTlem2VD  45625  iunord  50482