Theorem ordtr 6376

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

This proof depends on syntax axioms:   → wi 4  Tr wtr 5211   E cep 5549   We wwe 5602  Ord word 6361

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 6365

This theorem is used by:  ordelss  6378  ordn2lp  6382  ordelord  6384  tz7.7  6388  ordelssne  6389  ordin  6393  ordtr1  6407  orduniss  6462  ontr  6474  dford5  7798  ordsuci  7822  ordunisuc  7843  limsuc  7860  trom  7886  dfrecs3  8380  tz7.44-2  8415  cantnflt  9673  cantnfp1lem3  9681  cantnflem1b  9687  cantnflem1  9690  cnfcom  9701  axdc3lem2  10529  inar1  10860  efgmnvl  19928  bnj967  35575  dford3  44035  limsuc2  44048  ordsssucim  44404  ordelordALT  45520  onfrALTlem2  45529  ordelordALTVD  45849  onfrALTlem2VD  45871  iunord  50784