Theorem ordtr 6265

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

Syntax hints:   → wi 4  Tr wtr 5187   E cep 5485   We wwe 5534  Ord word 6250

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 206  df-an 396  df-ord 6254

This theorem is referenced by:  ordelss  6267  ordn2lp  6271  ordelord  6273  tz7.7  6277  ordelssne  6278  ordin  6281  ordtr1  6294  orduniss  6345  ontrci  6357  ordunisuc  7654  onuninsuci  7662  limsuc  7671  trom  7696  omsindsOLD  7709  dfrecs3  8174  dfrecs3OLD  8175  tz7.44-2  8209  cantnflt  9360  cantnfp1lem3  9368  cantnflem1b  9374  cantnflem1  9377  cnfcom  9388  axdc3lem2  10138  inar1  10462  efgmnvl  19235  bnj967  32825  dford5  33573  dford3  40766  limsuc2  40782  ordelordALT  42046  onfrALTlem2  42055  ordelordALTVD  42376  onfrALTlem2VD  42398  iunord  46268