Theorem cnvco 5833

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 1863	. . . 4 ⊢ (∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ↔ ∃𝑧(𝑧𝐴𝑦 ∧ 𝑥𝐵𝑧))
2		vex 3443	. . . . 5 ⊢ 𝑥 ∈ V
3		vex 3443	. . . . 5 ⊢ 𝑦 ∈ V
4	2, 3	brco 5818	. . . 4 ⊢ (𝑥(𝐴 ∘ 𝐵)𝑦 ↔ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦))
5		vex 3443	. . . . . . 7 ⊢ 𝑧 ∈ V
6	3, 5	brcnv 5830	. . . . . 6 ⊢ (𝑦◡𝐴𝑧 ↔ 𝑧𝐴𝑦)
7	5, 2	brcnv 5830	. . . . . 6 ⊢ (𝑧◡𝐵𝑥 ↔ 𝑥𝐵𝑧)
8	6, 7	anbi12i 629	. . . . 5 ⊢ ((𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥) ↔ (𝑧𝐴𝑦 ∧ 𝑥𝐵𝑧))
9	8	exbii 1850	. . . 4 ⊢ (∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥) ↔ ∃𝑧(𝑧𝐴𝑦 ∧ 𝑥𝐵𝑧))
10	1, 4, 9	3bitr4i 303	. . 3 ⊢ (𝑥(𝐴 ∘ 𝐵)𝑦 ↔ ∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥))
11	10	opabbii 5164	. 2 ⊢ {⟨𝑦, 𝑥⟩ ∣ 𝑥(𝐴 ∘ 𝐵)𝑦} = {⟨𝑦, 𝑥⟩ ∣ ∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥)}
12		df-cnv 5631	. 2 ⊢ ◡(𝐴 ∘ 𝐵) = {⟨𝑦, 𝑥⟩ ∣ 𝑥(𝐴 ∘ 𝐵)𝑦}
13		df-co 5632	. 2 ⊢ (◡𝐵 ∘ ◡𝐴) = {⟨𝑦, 𝑥⟩ ∣ ∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥)}
14	11, 12, 13	3eqtr4i 2768	1 ⊢ ◡(𝐴 ∘ 𝐵) = (◡𝐵 ∘ ◡𝐴)

Syntax hints:   ∧ wa 395   = wceq 1542  ∃wex 1781   class class class wbr 5097  {copab 5159  ^◡ccnv 5622   ∘ ccom 5627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707  ax-sep 5240  ax-nul 5250  ax-pr 5376

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-rab 3399  df-v 3441  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4285  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098  df-opab 5160  df-cnv 5631  df-co 5632

This theorem is referenced by:  rncoss  5925  rncoeq  5930  dmco  6212  cores2  6217  co01  6219  coi2  6221  relcnvtrg  6224  dfdm2  6238  f1cof1  6739  cofunex2g  7894  fparlem3  8056  fparlem4  8057  suppco  8148  fsuppcolem  9306  relexpcnv  14960  relexpaddg  14978  cnvps  18503  gimco  19199  gsumzf1o  19843  cnco  23212  ptrescn  23585  qtopcn  23660  hmeoco  23718  cncombf  25617  deg1val  26059  fcoinver  32659  ofpreima  32723  cycpmconjv  33203  cycpmconjs  33217  cyc3conja  33218  esplysply  33708  mbfmco  34400  eulerpartlemmf  34511  cvmliftmolem1  35454  cvmlift2lem9a  35476  cvmlift2lem9  35484  mclsppslem  35756  ftc1anclem3  37865  trlcocnv  41015  tendoicl  41091  cdlemk45  41242  rimco  42810  cononrel1  43872  cononrel2  43873  cnvtrcl0  43904  cnvtrrel  43948  relexpaddss  43996  frege131d  44042  brco2f1o  44310  brco3f1o  44311  clsneicnv  44383  neicvgnvo  44393  smfco  47083  upgrimpthslem1  48190  upgrimspths  48193