Theorem cnvco 5008

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	|- `' ( A o. B ) = ( `' B o. `' A )

Proof of Theorem cnvco

Dummy variables x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		exancom 1692	. . . 4 |- ( E. z ( x B z /\ z A y ) <-> E. z ( z A y /\ x B z ) )
2		vex 3061	. . . . 5 |- x e. _V
3		vex 3061	. . . . 5 |- y e. _V
4	2, 3	brco 4993	. . . 4 |- ( x ( A o. B ) y <-> E. z ( x B z /\ z A y ) )
5		vex 3061	. . . . . . 7 |- z e. _V
6	3, 5	brcnv 5005	. . . . . 6 |- ( y `' A z <-> z A y )
7	5, 2	brcnv 5005	. . . . . 6 |- ( z `' B x <-> x B z )
8	6, 7	anbi12i 695	. . . . 5 |- ( ( y `' A z /\ z `' B x ) <-> ( z A y /\ x B z ) )
9	8	exbii 1688	. . . 4 |- ( E. z ( y `' A z /\ z `' B x ) <-> E. z ( z A y /\ x B z ) )
10	1, 4, 9	3bitr4i 277	. . 3 |- ( x ( A o. B ) y <-> E. z ( y `' A z /\ z `' B x ) )
11	10	opabbii 4458	. 2 |- { <. y , x >. | x ( A o. B ) y } = { <. y , x >. | E. z ( y `' A z /\ z `' B x ) }
12		df-cnv 4830	. 2 |- `' ( A o. B ) = { <. y , x >. | x ( A o. B ) y }
13		df-co 4831	. 2 |- ( `' B o. `' A ) = { <. y , x >. | E. z ( y `' A z /\ z `' B x ) }
14	11, 12, 13	3eqtr4i 2441	1 |- `' ( A o. B ) = ( `' B o. `' A )

Syntax hints:   /\ wa 367   = wceq 1405   E.wex 1633   class class class wbr 4394   {copab 4451   `'ccnv 4821   o. ccom 4826

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pr 4629

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-rab 2762  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-br 4395  df-opab 4453  df-cnv 4830  df-co 4831

This theorem is referenced by:  rncoss  5083  rncoeq  5086  dmco  5330  cores2  5335  co01  5337  coi2  5339  relcnvtr  5342  dfdm2  5355  f1co  5772  cofunex2g  6748  fparlem3  6885  fparlem4  6886  supp0cosupp0  6941  imacosupp  6942  fsuppcolem  7893  mapfienOLD  8169  relexpcnv  13015  relexpaddg  13033  cnvps  16164  gimco  16638  gsumval3OLD  17230  gsumzf1o  17239  gsumzf1oOLD  17242  cnco  20058  ptrescn  20430  qtopcn  20505  hmeoco  20563  cncombf  22355  deg1val  22786  deg1valOLD  22787  fcoinver  27882  ofpreima  27936  mbfmco  28698  eulerpartlemmf  28806  cvmliftmolem1  29565  cvmlift2lem9a  29587  cvmlift2lem9  29595  mclsppslem  29782  ftc1anclem3  31445  trlcocnv  33719  tendoicl  33795  cdlemk45  33946  cnvtrrel  35629  relexpaddss  35677  frege131d  35723