Theorem cnvco 5867

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 1894	. . . 4 ⊢ (∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ↔ ∃𝑧(𝑧𝐴𝑦 ∧ 𝑥𝐵𝑧))
2		vex 3455	. . . . 5 ⊢ 𝑥 ∈ V
3		vex 3455	. . . . 5 ⊢ 𝑦 ∈ V
4	2, 3	brco 5848	. . . 4 ⊢ (𝑥(𝐴 ∘ 𝐵)𝑦 ↔ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦))
5		vex 3455	. . . . . . 7 ⊢ 𝑧 ∈ V
6	3, 5	brcnv 5860	. . . . . 6 ⊢ (𝑦◡𝐴𝑧 ↔ 𝑧𝐴𝑦)
7	5, 2	brcnv 5860	. . . . . 6 ⊢ (𝑧◡𝐵𝑥 ↔ 𝑥𝐵𝑧)
8	6, 7	anbi12i 640	. . . . 5 ⊢ ((𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥) ↔ (𝑧𝐴𝑦 ∧ 𝑥𝐵𝑧))
9	8	exbii 1881	. . . 4 ⊢ (∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥) ↔ ∃𝑧(𝑧𝐴𝑦 ∧ 𝑥𝐵𝑧))
10	1, 4, 9	3bitr4i 306	. . 3 ⊢ (𝑥(𝐴 ∘ 𝐵)𝑦 ↔ ∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥))
11	10	opabbii 5172	. 2 ⊢ {⟨𝑦, 𝑥⟩ ∣ 𝑥(𝐴 ∘ 𝐵)𝑦} = {⟨𝑦, 𝑥⟩ ∣ ∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥)}
12		df-cnv 5659	. 2 ⊢ ◡(𝐴 ∘ 𝐵) = {⟨𝑦, 𝑥⟩ ∣ 𝑥(𝐴 ∘ 𝐵)𝑦}
13		df-co 5660	. 2 ⊢ (◡𝐵 ∘ ◡𝐴) = {⟨𝑦, 𝑥⟩ ∣ ∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥)}
14	11, 12, 13	3eqtr4i 2794	1 ⊢ ◡(𝐴 ∘ 𝐵) = (◡𝐵 ∘ ◡𝐴)

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570  ∃wex 1812   class class class wbr 5103  {copab 5167  ^◡ccnv 5650   ∘ ccom 5655

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-cnv 5659  df-co 5660

This theorem is used by:  rncoss  5959  rncoeq  5963  dmco  6256  cores2  6261  co01  6263  coi2  6265  relcnvtrg  6268  relcnvtrgOLD  6269  dfdm2  6284  f1cof1  6790  cofunex2g  7962  fparlem3  8125  fparlem4  8126  suppco  8223  fsuppcolem  9393  relexpcnv  15188  relexpaddg  15206  cnvps  18752  gimco  19482  gsumzf1o  20126  rimco  20747  cnco  23584  ptrescn  23958  qtopcn  24033  hmeoco  24091  cncombf  25979  deg1val  26414  fcoinver  33198  ofpreima  33259  cycpmconjv  33703  cycpmconjs  33717  cyc3conja  33718  esplysply  34203  mbfmco  34896  eulerpartlemmf  35007  cvmliftmolem1  36046  cvmlift2lem9a  36068  cvmlift2lem9  36076  mclsppslem  36348  ftc1anclem3  38613  trlcocnv  41777  tendoicl  41853  cdlemk45  42004  cononrel1  44593  cononrel2  44594  cnvtrcl0  44625  cnvtrrel  44669  relexpaddss  44717  frege131d  44763  brco2f1o  45031  brco3f1o  45032  clsneicnv  45104  neicvgnvo  45114  cocanss1  45923  smfco  47811  upgrimpthslem1  49004  upgrimspths  49007