Theorem cnvco 5873

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 3458	. . . . 5 ⊢ 𝑥 ∈ V
3		vex 3458	. . . . 5 ⊢ 𝑦 ∈ V
4	2, 3	brco 5854	. . . 4 ⊢ (𝑥(𝐴 ∘ 𝐵)𝑦 ↔ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦))
5		vex 3458	. . . . . . 7 ⊢ 𝑧 ∈ V
6	3, 5	brcnv 5866	. . . . . 6 ⊢ (𝑦◡𝐴𝑧 ↔ 𝑧𝐴𝑦)
7	5, 2	brcnv 5866	. . . . . 6 ⊢ (𝑧◡𝐵𝑥 ↔ 𝑥𝐵𝑧)
8	6, 7	anbi12i 640	. . . . 5 ⊢ ((𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥) ↔ (𝑧𝐴𝑦 ∧ 𝑥𝐵𝑧))
9	8	exbii 1881	. . . 4 ⊢ (∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥) ↔ ∃𝑧(𝑧𝐴𝑦 ∧ 𝑥𝐵𝑧))
10	1, 4, 9	3bitr4i 306	. . 3 ⊢ (𝑥(𝐴 ∘ 𝐵)𝑦 ↔ ∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥))
11	10	opabbii 5175	. 2 ⊢ {⟨𝑦, 𝑥⟩ ∣ 𝑥(𝐴 ∘ 𝐵)𝑦} = {⟨𝑦, 𝑥⟩ ∣ ∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥)}
12		df-cnv 5663	. 2 ⊢ ◡(𝐴 ∘ 𝐵) = {⟨𝑦, 𝑥⟩ ∣ 𝑥(𝐴 ∘ 𝐵)𝑦}
13		df-co 5664	. 2 ⊢ (◡𝐵 ∘ ◡𝐴) = {⟨𝑦, 𝑥⟩ ∣ ∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥)}
14	11, 12, 13	3eqtr4i 2796	1 ⊢ ◡(𝐴 ∘ 𝐵) = (◡𝐵 ∘ ◡𝐴)

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570  ∃wex 1812   class class class wbr 5106  {copab 5170  ^◡ccnv 5654   ∘ ccom 5659

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-pr 5395

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  df-cnv 5663  df-co 5664

This theorem is used by:  rncoss  5965  rncoeq  5971  dmco  6268  cores2  6273  co01  6277  coi2  6279  relcnvtrg  6283  relcnvtrgOLD  6284  dfdm2  6299  f1cof1  6809  cofunex2g  7983  fparlem3  8149  fparlem4  8150  suppco  8248  fsuppcolem  9417  relexpcnv  15214  relexpaddg  15232  cnvps  18778  gimco  19508  gsumzf1o  20153  rimco  20774  cnco  23611  ptrescn  23985  qtopcn  24060  hmeoco  24118  cncombf  26006  deg1val  26441  fcoinver  33267  ofpreima  33328  cycpmconjv  33770  cycpmconjs  33784  cyc3conja  33785  esplysply  34270  mbfmco  34963  eulerpartlemmf  35074  cvmliftmolem1  36212  cvmlift2lem9a  36234  cvmlift2lem9  36242  mclsppslem  36514  ftc1anclem3  38804  trlcocnv  41968  tendoicl  42044  cdlemk45  42195  cononrel1  44784  cononrel2  44785  cnvtrcl0  44816  cnvtrrel  44860  relexpaddss  44908  frege131d  44954  brco2f1o  45222  brco3f1o  45223  clsneicnv  45295  neicvgnvo  45305  cocanss1  46114  smfco  48015  upgrimpthslem1  49208  upgrimspths  49211