Theorem cnvco 5864

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 3454	. . . . 5 ⊢ 𝑥 ∈ V
3		vex 3454	. . . . 5 ⊢ 𝑦 ∈ V
4	2, 3	brco 5845	. . . 4 ⊢ (𝑥(𝐴 ∘ 𝐵)𝑦 ↔ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦))
5		vex 3454	. . . . . . 7 ⊢ 𝑧 ∈ V
6	3, 5	brcnv 5857	. . . . . 6 ⊢ (𝑦◡𝐴𝑧 ↔ 𝑧𝐴𝑦)
7	5, 2	brcnv 5857	. . . . . 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 5656	. 2 ⊢ ◡(𝐴 ∘ 𝐵) = {⟨𝑦, 𝑥⟩ ∣ 𝑥(𝐴 ∘ 𝐵)𝑦}
13		df-co 5657	. 2 ⊢ (◡𝐵 ∘ ◡𝐴) = {⟨𝑦, 𝑥⟩ ∣ ∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥)}
14	11, 12, 13	3eqtr4i 2793	1 ⊢ ◡(𝐴 ∘ 𝐵) = (◡𝐵 ∘ ◡𝐴)

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

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 2732  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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  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 5656  df-co 5657

This theorem is used by:  rncoss  5956  rncoeq  5960  dmco  6246  cores2  6251  co01  6253  coi2  6255  relcnvtrg  6258  relcnvtrgOLD  6259  dfdm2  6274  f1cof1  6779  cofunex2g  7946  fparlem3  8109  fparlem4  8110  suppco  8202  fsuppcolem  9371  relexpcnv  15141  relexpaddg  15159  cnvps  18699  gimco  19429  gsumzf1o  20073  rimco  20694  cnco  23531  ptrescn  23905  qtopcn  23980  hmeoco  24038  cncombf  25926  deg1val  26361  fcoinver  33117  ofpreima  33178  cycpmconjv  33622  cycpmconjs  33636  cyc3conja  33637  esplysply  34122  mbfmco  34816  eulerpartlemmf  34927  cvmliftmolem1  35961  cvmlift2lem9a  35983  cvmlift2lem9  35991  mclsppslem  36263  ftc1anclem3  38527  trlcocnv  41691  tendoicl  41767  cdlemk45  41918  cononrel1  44532  cononrel2  44533  cnvtrcl0  44564  cnvtrrel  44608  relexpaddss  44656  frege131d  44702  brco2f1o  44970  brco3f1o  44971  clsneicnv  45043  neicvgnvo  45053  smfco  47728  upgrimpthslem1  48921  upgrimspths  48924