Theorem ordtr 6310

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

Syntax hints:   → wi 4  Tr wtr 5206   E cep 5517   We wwe 5568  Ord word 6295

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 6299

This theorem is referenced by:  ordelss  6312  ordn2lp  6316  ordelord  6318  tz7.7  6322  ordelssne  6323  ordin  6326  ordtr1  6339  orduniss  6392  ontr  6403  dford5  7688  ordsuci  7713  ordunisuc  7737  limsuc  7755  trom  7781  omsindsOLD  7794  dfrecs3  8265  dfrecs3OLD  8266  tz7.44-2  8300  cantnflt  9521  cantnfp1lem3  9529  cantnflem1b  9535  cantnflem1  9538  cnfcom  9549  axdc3lem2  10300  inar1  10624  efgmnvl  19407  bnj967  33137  dford3  41101  limsuc2  41117  ordelordALT  42467  onfrALTlem2  42476  ordelordALTVD  42797  onfrALTlem2VD  42819  iunord  46722