Theorem cnvco 5828

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 3440	. . . . 5 ⊢ 𝑥 ∈ V
3		vex 3440	. . . . 5 ⊢ 𝑦 ∈ V
4	2, 3	brco 5813	. . . 4 ⊢ (𝑥(𝐴 ∘ 𝐵)𝑦 ↔ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦))
5		vex 3440	. . . . . . 7 ⊢ 𝑧 ∈ V
6	3, 5	brcnv 5825	. . . . . 6 ⊢ (𝑦◡𝐴𝑧 ↔ 𝑧𝐴𝑦)
7	5, 2	brcnv 5825	. . . . . 6 ⊢ (𝑧◡𝐵𝑥 ↔ 𝑥𝐵𝑧)
8	6, 7	anbi12i 628	. . . . 5 ⊢ ((𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥) ↔ (𝑧𝐴𝑦 ∧ 𝑥𝐵𝑧))
9	8	exbii 1848	. . . 4 ⊢ (∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥) ↔ ∃𝑧(𝑧𝐴𝑦 ∧ 𝑥𝐵𝑧))
10	1, 4, 9	3bitr4i 303	. . 3 ⊢ (𝑥(𝐴 ∘ 𝐵)𝑦 ↔ ∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥))
11	10	opabbii 5159	. 2 ⊢ {⟨𝑦, 𝑥⟩ ∣ 𝑥(𝐴 ∘ 𝐵)𝑦} = {⟨𝑦, 𝑥⟩ ∣ ∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥)}
12		df-cnv 5627	. 2 ⊢ ◡(𝐴 ∘ 𝐵) = {⟨𝑦, 𝑥⟩ ∣ 𝑥(𝐴 ∘ 𝐵)𝑦}
13		df-co 5628	. 2 ⊢ (◡𝐵 ∘ ◡𝐴) = {⟨𝑦, 𝑥⟩ ∣ ∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥)}
14	11, 12, 13	3eqtr4i 2762	1 ⊢ ◡(𝐴 ∘ 𝐵) = (◡𝐵 ∘ ◡𝐴)

Syntax hints:   ∧ wa 395   = wceq 1540  ∃wex 1779   class class class wbr 5092  {copab 5154  ^◡ccnv 5618   ∘ ccom 5623

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 5235  ax-nul 5245  ax-pr 5371

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-cnv 5627  df-co 5628

This theorem is referenced by:  rncoss  5918  rncoeq  5923  dmco  6203  cores2  6208  co01  6210  coi2  6212  relcnvtrg  6215  dfdm2  6229  f1cof1  6730  cofunex2g  7885  fparlem3  8047  fparlem4  8048  suppco  8139  fsuppcolem  9291  relexpcnv  14942  relexpaddg  14960  cnvps  18484  gimco  19147  gsumzf1o  19791  cnco  23151  ptrescn  23524  qtopcn  23599  hmeoco  23657  cncombf  25557  deg1val  25999  fcoinver  32553  ofpreima  32616  cycpmconjv  33093  cycpmconjs  33107  cyc3conja  33108  mbfmco  34248  eulerpartlemmf  34359  cvmliftmolem1  35274  cvmlift2lem9a  35296  cvmlift2lem9  35304  mclsppslem  35576  ftc1anclem3  37695  trlcocnv  40719  tendoicl  40795  cdlemk45  40946  rimco  42511  cononrel1  43587  cononrel2  43588  cnvtrcl0  43619  cnvtrrel  43663  relexpaddss  43711  frege131d  43757  brco2f1o  44025  brco3f1o  44026  clsneicnv  44098  neicvgnvo  44108  smfco  46803  upgrimpthslem1  47911  upgrimspths  47914