Theorem ordtr 6363

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

Syntax hints:   → wi 4  Tr wtr 5211   E cep 5550   We wwe 5603  Ord word 6348

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 210  df-an 401  df-ord 6352

This theorem is referenced by:  ordelss  6365  ordn2lp  6369  ordelord  6371  tz7.7  6375  ordelssne  6376  ordin  6380  ordtr1  6394  orduniss  6449  ontr  6461  dford5  7771  ordsuci  7795  ordunisuc  7816  limsuc  7833  trom  7859  dfrecs3  8347  tz7.44-2  8382  cantnflt  9629  cantnfp1lem3  9637  cantnflem1b  9643  cantnflem1  9646  cnfcom  9657  axdc3lem2  10423  inar1  10748  efgmnvl  19772  bnj967  35245  dford3  43612  limsuc2  43625  ordsssucim  43986  ordelordALT  45105  onfrALTlem2  45114  ordelordALTVD  45434  onfrALTlem2VD  45456  iunord  50306