Theorem cnvco 5839

Description: Distributive law of converse over class composition. Theorem 26 of [Suppes] p. 64. (Contributed by NM, 19-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)

Assertion

Ref	Expression
cnvco	⊢ ◡(𝐴 ∘ 𝐵) = (◡𝐵 ∘ ◡𝐴)

Proof of Theorem cnvco

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		exancom 1861	. . . 4 ⊢ (∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ↔ ∃𝑧(𝑧𝐴𝑦 ∧ 𝑥𝐵𝑧))
2		vex 3448	. . . . 5 ⊢ 𝑥 ∈ V
3		vex 3448	. . . . 5 ⊢ 𝑦 ∈ V
4	2, 3	brco 5824	. . . 4 ⊢ (𝑥(𝐴 ∘ 𝐵)𝑦 ↔ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦))
5		vex 3448	. . . . . . 7 ⊢ 𝑧 ∈ V
6	3, 5	brcnv 5836	. . . . . 6 ⊢ (𝑦◡𝐴𝑧 ↔ 𝑧𝐴𝑦)
7	5, 2	brcnv 5836	. . . . . 6 ⊢ (𝑧◡𝐵𝑥 ↔ 𝑥𝐵𝑧)
8	6, 7	anbi12i 628	. . . . 5 ⊢ ((𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥) ↔ (𝑧𝐴𝑦 ∧ 𝑥𝐵𝑧))
9	8	exbii 1848	. . . 4 ⊢ (∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥) ↔ ∃𝑧(𝑧𝐴𝑦 ∧ 𝑥𝐵𝑧))
10	1, 4, 9	3bitr4i 303	. . 3 ⊢ (𝑥(𝐴 ∘ 𝐵)𝑦 ↔ ∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥))
11	10	opabbii 5169	. 2 ⊢ {⟨𝑦, 𝑥⟩ ∣ 𝑥(𝐴 ∘ 𝐵)𝑦} = {⟨𝑦, 𝑥⟩ ∣ ∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥)}
12		df-cnv 5639	. 2 ⊢ ◡(𝐴 ∘ 𝐵) = {⟨𝑦, 𝑥⟩ ∣ 𝑥(𝐴 ∘ 𝐵)𝑦}
13		df-co 5640	. 2 ⊢ (◡𝐵 ∘ ◡𝐴) = {⟨𝑦, 𝑥⟩ ∣ ∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥)}
14	11, 12, 13	3eqtr4i 2762	1 ⊢ ◡(𝐴 ∘ 𝐵) = (◡𝐵 ∘ ◡𝐴)

Syntax hints:   ∧ wa 395   = wceq 1540  ∃wex 1779   class class class wbr 5102  {copab 5164  ^◡ccnv 5630   ∘ ccom 5635

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-cnv 5639  df-co 5640

This theorem is referenced by:  rncoss  5928  rncoeq  5932  dmco  6215  cores2  6220  co01  6222  coi2  6224  relcnvtrg  6227  dfdm2  6242  f1cof1  6748  cofunex2g  7908  fparlem3  8070  fparlem4  8071  suppco  8162  fsuppcolem  9328  relexpcnv  14978  relexpaddg  14996  cnvps  18520  gimco  19183  gsumzf1o  19827  cnco  23187  ptrescn  23560  qtopcn  23635  hmeoco  23693  cncombf  25593  deg1val  26035  fcoinver  32584  ofpreima  32640  cycpmconjv  33115  cycpmconjs  33129  cyc3conja  33130  mbfmco  34249  eulerpartlemmf  34360  cvmliftmolem1  35262  cvmlift2lem9a  35284  cvmlift2lem9  35292  mclsppslem  35564  ftc1anclem3  37683  trlcocnv  40708  tendoicl  40784  cdlemk45  40935  rimco  42500  cononrel1  43577  cononrel2  43578  cnvtrcl0  43609  cnvtrrel  43653  relexpaddss  43701  frege131d  43747  brco2f1o  44015  brco3f1o  44016  clsneicnv  44088  neicvgnvo  44098  smfco  46794  upgrimpthslem1  47901  upgrimspths  47904