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

Theorem ordtr 4141
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 4130 . 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 2349   Tr wtr 3883   Ord word 4125
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 4129
This theorem is referenced by:  ordelss  4142  ordin  4148  ordtr1  4151  orduniss  4188  ontrci  4190  ordon  4238  ordsucim  4252  ordsucss  4256  onsucsssucr  4261  onintonm  4269  ordsucunielexmid  4282  ordn2lp  4296  onsucuni2  4315  nlimsucg  4317  ordpwsucss  4318  tfrexlem  5983  nnsucuniel  6139
  Copyright terms: Public domain W3C validator