Theorem cnvco 5036

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 1716	. . . 4 |- ( E. z ( x B z /\ z A y ) <-> E. z ( z A y /\ x B z ) )
2		vex 3084	. . . . 5 |- x e. _V
3		vex 3084	. . . . 5 |- y e. _V
4	2, 3	brco 5021	. . . 4 |- ( x ( A o. B ) y <-> E. z ( x B z /\ z A y ) )
5		vex 3084	. . . . . . 7 |- z e. _V
6	3, 5	brcnv 5033	. . . . . 6 |- ( y `' A z <-> z A y )
7	5, 2	brcnv 5033	. . . . . 6 |- ( z `' B x <-> x B z )
8	6, 7	anbi12i 701	. . . . 5 |- ( ( y `' A z /\ z `' B x ) <-> ( z A y /\ x B z ) )
9	8	exbii 1712	. . . 4 |- ( E. z ( y `' A z /\ z `' B x ) <-> E. z ( z A y /\ x B z ) )
10	1, 4, 9	3bitr4i 280	. . 3 |- ( x ( A o. B ) y <-> E. z ( y `' A z /\ z `' B x ) )
11	10	opabbii 4485	. 2 |- { <. y , x >. | x ( A o. B ) y } = { <. y , x >. | E. z ( y `' A z /\ z `' B x ) }
12		df-cnv 4858	. 2 |- `' ( A o. B ) = { <. y , x >. | x ( A o. B ) y }
13		df-co 4859	. 2 |- ( `' B o. `' A ) = { <. y , x >. | E. z ( y `' A z /\ z `' B x ) }
14	11, 12, 13	3eqtr4i 2461	1 |- `' ( A o. B ) = ( `' B o. `' A )

Syntax hints:   /\ wa 370   = wceq 1437   E.wex 1659   class class class wbr 4420   {copab 4478   `'ccnv 4849   o. ccom 4854

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pr 4657

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-rab 2784  df-v 3083  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-br 4421  df-opab 4480  df-cnv 4858  df-co 4859

This theorem is referenced by:  rncoss  5111  rncoeq  5114  dmco  5359  cores2  5364  co01  5366  coi2  5368  relcnvtr  5371  dfdm2  5384  f1co  5802  cofunex2g  6769  fparlem3  6906  fparlem4  6907  supp0cosupp0  6962  imacosupp  6963  fsuppcolem  7917  relexpcnv  13087  relexpaddg  13105  cnvps  16446  gimco  16920  gsumzf1o  17534  cnco  20269  ptrescn  20641  qtopcn  20716  hmeoco  20774  cncombf  22601  deg1val  23032  fcoinver  28204  ofpreima  28258  mbfmco  29082  eulerpartlemmf  29204  cvmliftmolem1  30000  cvmlift2lem9a  30022  cvmlift2lem9  30030  mclsppslem  30217  ftc1anclem3  31933  trlcocnv  34206  tendoicl  34282  cdlemk45  34433  cnvtrrel  36122  relexpaddss  36170  frege131d  36216