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

Theorem ordtr 4270
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 4259 . 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 2393   Tr wtr 3996   Ord word 4254
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 4258
This theorem is referenced by:  ordelss  4271  ordin  4277  ordtr1  4280  orduniss  4317  ontrci  4319  ordon  4372  ordsucim  4386  ordsucss  4390  onsucsssucr  4395  onintonm  4403  ordsucunielexmid  4416  ordn2lp  4430  onsucuni2  4449  nlimsucg  4451  ordpwsucss  4452  tfrexlem  6199  nnsucuniel  6359  ctmlemr  6961  nnnninf  6991  ctinf  11870  nnsf  13126  peano4nninf  13127  nninfalllemn  13129
  Copyright terms: Public domain W3C validator