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

Theorem sotri 4814
Description: A strict order relation is a transitive relation. (Contributed by NM, 10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.)
Hypotheses
Ref Expression
soi.1 𝑅 Or 𝑆
soi.2 𝑅 ⊆ (𝑆 × 𝑆)
Assertion
Ref Expression
sotri ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐴𝑅𝐶)

Proof of Theorem sotri
StepHypRef Expression
1 soi.2 . . . . 5 𝑅 ⊆ (𝑆 × 𝑆)
21brel 4478 . . . 4 (𝐴𝑅𝐵 → (𝐴𝑆𝐵𝑆))
32simpld 110 . . 3 (𝐴𝑅𝐵𝐴𝑆)
41brel 4478 . . 3 (𝐵𝑅𝐶 → (𝐵𝑆𝐶𝑆))
53, 4anim12i 331 . 2 ((𝐴𝑅𝐵𝐵𝑅𝐶) → (𝐴𝑆 ∧ (𝐵𝑆𝐶𝑆)))
6 soi.1 . . . 4 𝑅 Or 𝑆
7 sotr 4136 . . . 4 ((𝑅 Or 𝑆 ∧ (𝐴𝑆𝐵𝑆𝐶𝑆)) → ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐴𝑅𝐶))
86, 7mpan 415 . . 3 ((𝐴𝑆𝐵𝑆𝐶𝑆) → ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐴𝑅𝐶))
983expb 1144 . 2 ((𝐴𝑆 ∧ (𝐵𝑆𝐶𝑆)) → ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐴𝑅𝐶))
105, 9mpcom 36 1 ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐴𝑅𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  w3a 924  wcel 1438  wss 2997   class class class wbr 3837   Or wor 4113   × cxp 4426
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-sep 3949  ax-pow 4001  ax-pr 4027
This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364  df-rex 2365  df-v 2621  df-un 3001  df-in 3003  df-ss 3010  df-pw 3427  df-sn 3447  df-pr 3448  df-op 3450  df-br 3838  df-opab 3892  df-po 4114  df-iso 4115  df-xp 4434
This theorem is referenced by:  son2lpi  4815  ltsonq  6936  lt2addnq  6942  lt2mulnq  6943  ltbtwnnqq  6953  prarloclemarch2  6957  genplt2i  7048  addlocprlemgt  7072  nqprloc  7083  prmuloclemcalc  7103  ltsopr  7134  ltexprlemopl  7139  ltexprlemopu  7141  ltexprlemru  7150  prplnqu  7158  recexprlemlol  7164  recexprlemupu  7166  recexprlemdisj  7168  recexprlemss1l  7173  recexprlemss1u  7174  cauappcvgprlemopl  7184  cauappcvgprlemlol  7185  cauappcvgprlemupu  7187  cauappcvgprlemladdfu  7192  caucvgprlemk  7203  caucvgprlemnkj  7204  caucvgprlemnbj  7205  caucvgprlemm  7206  caucvgprlemopl  7207  caucvgprlemlol  7208  caucvgprlemupu  7210  caucvgprlemloc  7213  caucvgprlemladdfu  7215  caucvgprprlemk  7221  caucvgprprlemloccalc  7222  caucvgprprlemnkltj  7227  caucvgprprlemnkeqj  7228  caucvgprprlemnjltk  7229  caucvgprprlemnbj  7231  caucvgprprlemml  7232  caucvgprprlemopl  7235  caucvgprprlemlol  7236  caucvgprprlemupu  7238  lttrsr  7287  addgt0sr  7300  archsr  7306  caucvgsrlemcl  7313  caucvgsrlemfv  7315  axpre-lttrn  7398
  Copyright terms: Public domain W3C validator