Theorem ordtr 6336

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

Syntax hints:   → wi 4  Tr wtr 5227   E cep 5541   We wwe 5592  Ord word 6321

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 397  df-ord 6325

This theorem is referenced by:  ordelss  6338  ordn2lp  6342  ordelord  6344  tz7.7  6348  ordelssne  6349  ordin  6352  ordtr1  6365  orduniss  6419  ontr  6431  dford5  7723  ordsuci  7748  ordunisuc  7772  limsuc  7790  trom  7816  omsindsOLD  7829  dfrecs3  8323  dfrecs3OLD  8324  tz7.44-2  8358  cantnflt  9617  cantnfp1lem3  9625  cantnflem1b  9631  cantnflem1  9634  cnfcom  9645  axdc3lem2  10396  inar1  10720  efgmnvl  19510  bnj967  33646  dford3  41410  limsuc2  41426  ordsssucim  41796  ordelordALT  42941  onfrALTlem2  42950  ordelordALTVD  43271  onfrALTlem2VD  43293  iunord  47241