MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ordtr1 Structured version   Visualization version   Unicode version

Theorem ordtr1 5466
Description: Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004.)
Assertion
Ref Expression
ordtr1  |-  ( Ord 
C  ->  ( ( A  e.  B  /\  B  e.  C )  ->  A  e.  C ) )

Proof of Theorem ordtr1
StepHypRef Expression
1 ordtr 5437 . 2  |-  ( Ord 
C  ->  Tr  C
)
2 trel 4504 . 2  |-  ( Tr  C  ->  ( ( A  e.  B  /\  B  e.  C )  ->  A  e.  C ) )
31, 2syl 17 1  |-  ( Ord 
C  ->  ( ( A  e.  B  /\  B  e.  C )  ->  A  e.  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    e. wcel 1887   Tr wtr 4497   Ord word 5422
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-v 3047  df-in 3411  df-ss 3418  df-uni 4199  df-tr 4498  df-ord 5426
This theorem is referenced by:  ontr1  5469  dfsmo2  7066  smores2  7073  smoel  7079  smogt  7086  ordiso2  8030  r1ordg  8249  r1pwss  8255  r1val1  8257  rankr1ai  8269  rankval3b  8297  rankonidlem  8299  onssr1  8302  cofsmo  8699  fpwwe2lem9  9063  bnj1098  29595  bnj594  29723
  Copyright terms: Public domain W3C validator