Theorem ordtr 6391

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

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

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 6380

This theorem is used by:  ordelss  6393  ordn2lp  6397  ordelord  6399  tz7.7  6403  ordelssne  6404  ordin  6408  ordtr1  6422  orduniss  6477  ontr  6489  dford5  7819  ordsuci  7843  limsuc  7881  trom  7907  dfrecs3  8405  tz7.44-2  8440  cantnflt  9697  cantnfp1lem3  9705  cantnflem1b  9711  cantnflem1  9714  cnfcom  9725  axdc3lem2  10553  inar1  10884  efgmnvl  19955  bnj967  35642  dford3  44226  limsuc2  44239  ordsssucim  44594  ordelordALT  45709  onfrALTlem2  45718  ordelordALTVD  46038  onfrALTlem2VD  46060  iunord  51062