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

Theorem ordtr 4300
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 4289 . 2  |-  ( Ord 
A  <->  ( Tr  A  /\  A. x  e.  A  Tr  x ) )
21simplbi 272 1  |-  ( Ord 
A  ->  Tr  A
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wral 2416   Tr wtr 4026   Ord word 4284
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116  df-iord 4288
This theorem is referenced by:  ordelss  4301  ordin  4307  ordtr1  4310  orduniss  4347  ontrci  4349  ordon  4402  ordsucim  4416  ordsucss  4420  onsucsssucr  4425  onintonm  4433  ordsucunielexmid  4446  ordn2lp  4460  onsucuni2  4479  nlimsucg  4481  ordpwsucss  4482  tfrexlem  6231  nnsucuniel  6391  ctmlemr  6993  nnnninf  7023  ctinf  11954  nnsf  13285  peano4nninf  13286  nninfalllemn  13288
  Copyright terms: Public domain W3C validator