Theorem ordtr 6188

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

Syntax hints:   → wi 4  Tr wtr 5142   E cep 5438   We wwe 5486  Ord word 6173

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 400  df-ord 6177

This theorem is referenced by:  ordelss  6190  ordn2lp  6194  ordelord  6196  tz7.7  6200  ordelssne  6201  ordin  6204  ordtr1  6217  orduniss  6268  ontrci  6280  ordunisuc  7552  onuninsuci  7560  limsuc  7569  ordom  7594  elnn  7595  omsinds  7605  dfrecs3  8025  tz7.44-2  8059  cantnflt  9181  cantnfp1lem3  9189  cantnflem1b  9195  cantnflem1  9198  cnfcom  9209  axdc3lem2  9924  inar1  10248  efgmnvl  18920  bnj967  32457  dford5  33201  dford3  40377  limsuc2  40393  ordelordALT  41651  onfrALTlem2  41660  ordelordALTVD  41981  onfrALTlem2VD  42003  iunord  45691