Theorem ordtr 5955

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

Syntax hints:   → wi 4  Tr wtr 4945   E cep 5224   We wwe 5270  Ord word 5940

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 199  df-an 386  df-ord 5944

This theorem is referenced by:  ordelss  5957  ordn2lp  5961  ordelord  5963  tz7.7  5967  ordelssne  5968  ordin  5971  ordtr1  5984  orduniss  6035  ontrci  6046  ordunisuc  7266  onuninsuci  7274  limsuc  7283  ordom  7308  elnn  7309  omsinds  7318  dfrecs3  7708  tz7.44-2  7742  cantnflt  8819  cantnfp1lem3  8827  cantnflem1b  8833  cantnflem1  8836  cnfcom  8847  axdc3lem2  9561  inar1  9885  efgmnvl  18440  bnj967  31532  dford5  32123  dford3  38376  limsuc2  38392  ordelordALT  39519  onfrALTlem2  39528  ordelordALTVD  39859  onfrALTlem2VD  39881  iunord  43217