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 3457	. . . . 5 ⊢ 𝑥 ∈ V
3		vex 3457	. . . . 5 ⊢ 𝑦 ∈ V
4	2, 3	brco 5854	. . . 4 ⊢ (𝑥(𝐴 ∘ 𝐵)𝑦 ↔ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦))
5		vex 3457	. . . . . . 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 5176	. 2 ⊢ {⟨𝑦, 𝑥⟩ ∣ 𝑥(𝐴 ∘ 𝐵)𝑦} = {⟨𝑦, 𝑥⟩ ∣ ∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥)}
12		df-cnv 5667	. 2 ⊢ ◡(𝐴 ∘ 𝐵) = {⟨𝑦, 𝑥⟩ ∣ 𝑥(𝐴 ∘ 𝐵)𝑦}
13		df-co 5668	. 2 ⊢ (◡𝐵 ∘ ◡𝐴) = {⟨𝑦, 𝑥⟩ ∣ ∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥)}
14	11, 12, 13	3eqtr4i 2795	1 ⊢ ◡(𝐴 ∘ 𝐵) = (◡𝐵 ∘ ◡𝐴)

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570  ∃wex 1812   class class class wbr 5107  {copab 5171  ^◡ccnv 5658   ∘ ccom 5663

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 2734  ax-sep 5255  ax-pr 5402

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 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-cnv 5667  df-co 5668

This theorem is used by:  rncoss  5965  rncoeq  5969  dmco  6255  cores2  6260  co01  6262  coi2  6264  relcnvtrg  6267  relcnvtrgOLD  6268  dfdm2  6283  f1cof1  6787  cofunex2g  7950  fparlem3  8114  fparlem4  8115  suppco  8207  fsuppcolem  9374  relexpcnv  15110  relexpaddg  15128  cnvps  18670  gimco  19396  gsumzf1o  20040  rimco  20659  cnco  23492  ptrescn  23866  qtopcn  23941  hmeoco  23999  cncombf  25887  deg1val  26323  fcoinver  33064  ofpreima  33125  cycpmconjv  33569  cycpmconjs  33583  cyc3conja  33584  esplysply  34068  mbfmco  34762  eulerpartlemmf  34873  cvmliftmolem1  35847  cvmlift2lem9a  35869  cvmlift2lem9  35877  mclsppslem  36149  ftc1anclem3  38431  trlcocnv  41580  tendoicl  41656  cdlemk45  41807  cononrel1  44421  cononrel2  44422  cnvtrcl0  44453  cnvtrrel  44497  relexpaddss  44545  frege131d  44591  brco2f1o  44859  brco3f1o  44860  clsneicnv  44932  neicvgnvo  44942  smfco  47617  upgrimpthslem1  48810  upgrimspths  48813