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

Theorem sotri 4902
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 4559 . . . 4 (𝐴𝑅𝐵 → (𝐴𝑆𝐵𝑆))
32simpld 111 . . 3 (𝐴𝑅𝐵𝐴𝑆)
41brel 4559 . . 3 (𝐵𝑅𝐶 → (𝐵𝑆𝐶𝑆))
53, 4anim12i 334 . 2 ((𝐴𝑅𝐵𝐵𝑅𝐶) → (𝐴𝑆 ∧ (𝐵𝑆𝐶𝑆)))
6 soi.1 . . . 4 𝑅 Or 𝑆
7 sotr 4208 . . . 4 ((𝑅 Or 𝑆 ∧ (𝐴𝑆𝐵𝑆𝐶𝑆)) → ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐴𝑅𝐶))
86, 7mpan 418 . . 3 ((𝐴𝑆𝐵𝑆𝐶𝑆) → ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐴𝑅𝐶))
983expb 1165 . 2 ((𝐴𝑆 ∧ (𝐵𝑆𝐶𝑆)) → ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐴𝑅𝐶))
105, 9mpcom 36 1 ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐴𝑅𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 945  wcel 1463  wss 3039   class class class wbr 3897   Or wor 4185   × cxp 4505
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4014  ax-pow 4066  ax-pr 4099
This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ral 2396  df-rex 2397  df-v 2660  df-un 3043  df-in 3045  df-ss 3052  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-br 3898  df-opab 3958  df-po 4186  df-iso 4187  df-xp 4513
This theorem is referenced by:  son2lpi  4903  ltsonq  7170  lt2addnq  7176  lt2mulnq  7177  ltbtwnnqq  7187  prarloclemarch2  7191  genplt2i  7282  addlocprlemgt  7306  nqprloc  7317  prmuloclemcalc  7337  ltsopr  7368  ltexprlemopl  7373  ltexprlemopu  7375  ltexprlemru  7384  prplnqu  7392  recexprlemlol  7398  recexprlemupu  7400  recexprlemdisj  7402  recexprlemss1l  7407  recexprlemss1u  7408  cauappcvgprlemopl  7418  cauappcvgprlemlol  7419  cauappcvgprlemupu  7421  cauappcvgprlemladdfu  7426  caucvgprlemk  7437  caucvgprlemnkj  7438  caucvgprlemnbj  7439  caucvgprlemm  7440  caucvgprlemopl  7441  caucvgprlemlol  7442  caucvgprlemupu  7444  caucvgprlemloc  7447  caucvgprlemladdfu  7449  caucvgprprlemk  7455  caucvgprprlemloccalc  7456  caucvgprprlemnkltj  7461  caucvgprprlemnkeqj  7462  caucvgprprlemnjltk  7463  caucvgprprlemnbj  7465  caucvgprprlemml  7466  caucvgprprlemopl  7469  caucvgprprlemlol  7470  caucvgprprlemupu  7472  lttrsr  7534  addgt0sr  7547  archsr  7554  caucvgsrlemcl  7561  caucvgsrlemfv  7563  suplocsrlemb  7578  suplocsrlempr  7579  suplocsrlem  7580  axpre-lttrn  7656
  Copyright terms: Public domain W3C validator