ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ordtr Unicode version

Theorem ordtr 4203
Description: An ordinal class is transitive. (Contributed by NM, 3-Apr-1994.)
Assertion
Ref Expression
ordtr  |-  ( Ord 
A  ->  Tr  A
)

Proof of Theorem ordtr
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 dford3 4192 . 2  |-  ( Ord 
A  <->  ( Tr  A  /\  A. x  e.  A  Tr  x ) )
21simplbi 268 1  |-  ( Ord 
A  ->  Tr  A
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wral 2359   Tr wtr 3934   Ord word 4187
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115  df-iord 4191
This theorem is referenced by:  ordelss  4204  ordin  4210  ordtr1  4213  orduniss  4250  ontrci  4252  ordon  4301  ordsucim  4315  ordsucss  4319  onsucsssucr  4324  onintonm  4332  ordsucunielexmid  4345  ordn2lp  4359  onsucuni2  4378  nlimsucg  4380  ordpwsucss  4381  tfrexlem  6091  nnsucuniel  6248  nnnninf  6796  nnsf  11778  peano4nninf  11779  nninfalllemn  11781
  Copyright terms: Public domain W3C validator