Theorem ordtr 6373

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

This proof depends on syntax axioms:   → wi 4  Tr wtr 5212   E cep 5554   We wwe 5607  Ord word 6358

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 402  df-ord 6362

This theorem is used by:  ordelss  6375  ordn2lp  6379  ordelord  6381  tz7.7  6385  ordelssne  6386  ordin  6390  ordtr1  6404  orduniss  6459  ontr  6471  dford5  7789  ordsuci  7813  ordunisuc  7834  limsuc  7851  trom  7877  dfrecs3  8366  tz7.44-2  8401  cantnflt  9658  cantnfp1lem3  9666  cantnflem1b  9672  cantnflem1  9675  cnfcom  9686  axdc3lem2  10478  inar1  10809  efgmnvl  19867  bnj967  35487  dford3  43934  limsuc2  43947  ordsssucim  44308  ordelordALT  45425  onfrALTlem2  45434  ordelordALTVD  45754  onfrALTlem2VD  45776  iunord  50667