Theorem cnvco 5852

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

Syntax hints:   ∧ wa 395   = wceq 1540  ∃wex 1779   class class class wbr 5110  {copab 5172  ^◡ccnv 5640   ∘ ccom 5645

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-cnv 5649  df-co 5650

This theorem is referenced by:  rncoss  5942  rncoeq  5946  dmco  6230  cores2  6235  co01  6237  coi2  6239  relcnvtrg  6242  dfdm2  6257  f1cof1  6769  cofunex2g  7931  fparlem3  8096  fparlem4  8097  suppco  8188  fsuppcolem  9359  relexpcnv  15008  relexpaddg  15026  cnvps  18544  gimco  19207  gsumzf1o  19849  cnco  23160  ptrescn  23533  qtopcn  23608  hmeoco  23666  cncombf  25566  deg1val  26008  fcoinver  32540  ofpreima  32596  cycpmconjv  33106  cycpmconjs  33120  cyc3conja  33121  mbfmco  34262  eulerpartlemmf  34373  cvmliftmolem1  35275  cvmlift2lem9a  35297  cvmlift2lem9  35305  mclsppslem  35577  ftc1anclem3  37696  trlcocnv  40721  tendoicl  40797  cdlemk45  40948  rimco  42513  cononrel1  43590  cononrel2  43591  cnvtrcl0  43622  cnvtrrel  43666  relexpaddss  43714  frege131d  43760  brco2f1o  44028  brco3f1o  44029  clsneicnv  44101  neicvgnvo  44111  smfco  46807  upgrimpthslem1  47911  upgrimspths  47914