Theorem ordtr 6375

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

This proof depends on syntax axioms:   → wi 4  Tr wtr 5216   E cep 5558   We wwe 5611  Ord word 6360

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 6364

This theorem is used by:  ordelss  6377  ordn2lp  6381  ordelord  6383  tz7.7  6387  ordelssne  6388  ordin  6392  ordtr1  6406  orduniss  6461  ontr  6473  dford5  7786  ordsuci  7810  ordunisuc  7831  limsuc  7848  trom  7874  dfrecs3  8364  tz7.44-2  8399  cantnflt  9654  cantnfp1lem3  9662  cantnflem1b  9668  cantnflem1  9671  cnfcom  9682  axdc3lem2  10456  inar1  10785  efgmnvl  19840  bnj967  35439  dford3  43854  limsuc2  43867  ordsssucim  44228  ordelordALT  45345  onfrALTlem2  45354  ordelordALTVD  45674  onfrALTlem2VD  45696  iunord  50587