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 1869	. . . 4 ⊢ (∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ↔ ∃𝑧(𝑧𝐴𝑦 ∧ 𝑥𝐵𝑧))
2		vex 3437	. . . . 5 ⊢ 𝑥 ∈ V
3		vex 3437	. . . . 5 ⊢ 𝑦 ∈ V
4	2, 3	brco 5814	. . . 4 ⊢ (𝑥(𝐴 ∘ 𝐵)𝑦 ↔ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦))
5		vex 3437	. . . . . . 7 ⊢ 𝑧 ∈ V
6	3, 5	brcnv 5826	. . . . . 6 ⊢ (𝑦◡𝐴𝑧 ↔ 𝑧𝐴𝑦)
7	5, 2	brcnv 5826	. . . . . 6 ⊢ (𝑧◡𝐵𝑥 ↔ 𝑥𝐵𝑧)
8	6, 7	anbi12i 635	. . . . 5 ⊢ ((𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥) ↔ (𝑧𝐴𝑦 ∧ 𝑥𝐵𝑧))
9	8	exbii 1856	. . . 4 ⊢ (∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥) ↔ ∃𝑧(𝑧𝐴𝑦 ∧ 𝑥𝐵𝑧))
10	1, 4, 9	3bitr4i 305	. . 3 ⊢ (𝑥(𝐴 ∘ 𝐵)𝑦 ↔ ∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥))
11	10	opabbii 5141	. 2 ⊢ {⟨𝑦, 𝑥⟩ ∣ 𝑥(𝐴 ∘ 𝐵)𝑦} = {⟨𝑦, 𝑥⟩ ∣ ∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥)}
12		df-cnv 5628	. 2 ⊢ ◡(𝐴 ∘ 𝐵) = {⟨𝑦, 𝑥⟩ ∣ 𝑥(𝐴 ∘ 𝐵)𝑦}
13		df-co 5629	. 2 ⊢ (◡𝐵 ∘ ◡𝐴) = {⟨𝑦, 𝑥⟩ ∣ ∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥)}
14	11, 12, 13	3eqtr4i 2774	1 ⊢ ◡(𝐴 ∘ 𝐵) = (◡𝐵 ∘ ◡𝐴)

Syntax hints:   ∧ wa 397   = wceq 1548  ∃wex 1787   class class class wbr 5074  {copab 5136  ^◡ccnv 5619   ∘ ccom 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5220  ax-pr 5364

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-br 5075  df-opab 5137  df-cnv 5628  df-co 5629

This theorem is referenced by:  rncoss  5925  rncoeq  5930  dmco  6209  cores2  6214  co01  6216  coi2  6218  relcnvtrg  6221  dfdm2  6235  f1cof1  6736  cofunex2g  7894  fparlem3  8055  fparlem4  8056  suppco  8148  fsuppcolem  9308  relexpcnv  14992  relexpaddg  15010  cnvps  18539  gimco  19237  gsumzf1o  19881  cnco  23252  ptrescn  23625  qtopcn  23700  hmeoco  23758  cncombf  25646  deg1val  26082  fcoinver  32695  ofpreima  32759  cycpmconjv  33225  cycpmconjs  33239  cyc3conja  33240  esplysply  33765  mbfmco  34458  eulerpartlemmf  34569  cvmliftmolem1  35522  cvmlift2lem9a  35544  cvmlift2lem9  35552  mclsppslem  35824  ftc1anclem3  38075  trlcocnv  41225  tendoicl  41301  cdlemk45  41452  rimco  43018  cononrel1  44051  cononrel2  44052  cnvtrcl0  44083  cnvtrrel  44127  relexpaddss  44175  frege131d  44221  brco2f1o  44489  brco3f1o  44490  clsneicnv  44562  neicvgnvo  44572  smfco  47257  upgrimpthslem1  48410  upgrimspths  48413