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

Theorem ontr2 4615
Description: Transitive law for ordinal numbers. Exercise 3 of [TakeutiZaring] p. 40. (Contributed by NM, 6-Nov-2003.)
Assertion
Ref Expression
ontr2  |-  ( ( A  e.  On  /\  C  e.  On )  ->  ( ( A  C_  B  /\  B  e.  C
)  ->  A  e.  C ) )

Proof of Theorem ontr2
StepHypRef Expression
1 eloni 4578 . 2  |-  ( A  e.  On  ->  Ord  A )
2 eloni 4578 . 2  |-  ( C  e.  On  ->  Ord  C )
3 ordtr2 4612 . 2  |-  ( ( Ord  A  /\  Ord  C )  ->  ( ( A  C_  B  /\  B  e.  C )  ->  A  e.  C ) )
41, 2, 3syl2an 464 1  |-  ( ( A  e.  On  /\  C  e.  On )  ->  ( ( A  C_  B  /\  B  e.  C
)  ->  A  e.  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1725    C_ wss 3307   Ord word 4567   Oncon0 4568
This theorem is referenced by:  oeordsuc  6823  oelimcl  6829  oeeui  6831  omopthlem2  6885  omxpenlem  7195  oismo  7493  cantnflem1c  7627  cantnflem1  7629  cantnflem3  7631  rankr1ai  7708  rankxplim  7787  infxpenlem  7879  alephle  7953  pwcfsdom  8442  r1limwun  8595  nobndlem6  25601  ontopbas  26121  ontgval  26124
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411  ax-sep 4317  ax-nul 4325  ax-pr 4390
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-ne 2595  df-ral 2697  df-rex 2698  df-rab 2701  df-v 2945  df-sbc 3149  df-dif 3310  df-un 3312  df-in 3314  df-ss 3321  df-pss 3323  df-nul 3616  df-if 3727  df-sn 3807  df-pr 3808  df-op 3810  df-uni 4003  df-br 4200  df-opab 4254  df-tr 4290  df-eprel 4481  df-po 4490  df-so 4491  df-fr 4528  df-we 4530  df-ord 4571  df-on 4572
  Copyright terms: Public domain W3C validator