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

Theorem caovord2d 5796
Description: Operation ordering law with commuted arguments. (Contributed by Mario Carneiro, 30-Dec-2014.)
Hypotheses
Ref Expression
caovordg.1 ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦)))
caovordd.2 (𝜑𝐴𝑆)
caovordd.3 (𝜑𝐵𝑆)
caovordd.4 (𝜑𝐶𝑆)
caovord2d.com ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))
Assertion
Ref Expression
caovord2d (𝜑 → (𝐴𝑅𝐵 ↔ (𝐴𝐹𝐶)𝑅(𝐵𝐹𝐶)))
Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝑥,𝐵,𝑦,𝑧   𝑥,𝐶,𝑦,𝑧   𝜑,𝑥,𝑦,𝑧   𝑥,𝐹,𝑦,𝑧   𝑥,𝑅,𝑦,𝑧   𝑥,𝑆,𝑦,𝑧

Proof of Theorem caovord2d
StepHypRef Expression
1 caovordg.1 . . 3 ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦)))
2 caovordd.2 . . 3 (𝜑𝐴𝑆)
3 caovordd.3 . . 3 (𝜑𝐵𝑆)
4 caovordd.4 . . 3 (𝜑𝐶𝑆)
51, 2, 3, 4caovordd 5795 . 2 (𝜑 → (𝐴𝑅𝐵 ↔ (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵)))
6 caovord2d.com . . . 4 ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))
76, 4, 2caovcomd 5783 . . 3 (𝜑 → (𝐶𝐹𝐴) = (𝐴𝐹𝐶))
86, 4, 3caovcomd 5783 . . 3 (𝜑 → (𝐶𝐹𝐵) = (𝐵𝐹𝐶))
97, 8breq12d 3850 . 2 (𝜑 → ((𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵) ↔ (𝐴𝐹𝐶)𝑅(𝐵𝐹𝐶)))
105, 9bitrd 186 1 (𝜑 → (𝐴𝑅𝐵 ↔ (𝐴𝐹𝐶)𝑅(𝐵𝐹𝐶)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103  w3a 924   = wceq 1289  wcel 1438   class class class wbr 3837  (class class class)co 5634
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-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-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
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-sn 3447  df-pr 3448  df-op 3450  df-uni 3649  df-br 3838  df-iota 4967  df-fv 5010  df-ov 5637
This theorem is referenced by:  caovord3d  5797  genplt2i  7048  addnqprllem  7065  addnqprulem  7066  mulnqprl  7106  mulnqpru  7107  distrlem4prl  7122  distrlem4pru  7123  1idprl  7128  1idpru  7129  ltexprlemdisj  7144  ltexprlemloc  7145  ltexprlemfl  7147  ltexprlemfu  7149  prplnqu  7158  recexprlem1ssl  7171  recexprlem1ssu  7172  aptiprleml  7177  aptiprlemu  7178  caucvgprlemcanl  7182  cauappcvgprlemlol  7185  cauappcvgprlemloc  7190  cauappcvgprlemladdfu  7192  cauappcvgprlemladdru  7194  cauappcvgprlemladdrl  7195  cauappcvgprlem1  7197  caucvgprlemnkj  7204  caucvgprlemnbj  7205  caucvgprlemlol  7208  caucvgprlemloc  7213  caucvgprlemladdfu  7215  caucvgprlemladdrl  7216  caucvgprprlemnkltj  7227  caucvgprprlemnbj  7231  caucvgprprlemmu  7233  caucvgprprlemlol  7236  caucvgprprlemloc  7241  caucvgprprlemexbt  7244  caucvgprprlemexb  7245  caucvgprprlemaddq  7246  lttrsr  7287  ltsosr  7289  prsrlt  7311  caucvgsrlemoffcau  7322  caucvgsrlemoffgt1  7323  caucvgsrlemoffres  7324  caucvgsr  7326
  Copyright terms: Public domain W3C validator