MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnvco Unicode version

Theorem cnvco 4864
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.
StepHypRef Expression
1 exancom 1573 . . . 4  |-  ( E. z ( x B z  /\  z A y )  <->  E. z
( z A y  /\  x B z ) )
2 vex 2792 . . . . 5  |-  x  e. 
_V
3 vex 2792 . . . . 5  |-  y  e. 
_V
42, 3brco 4851 . . . 4  |-  ( x ( A  o.  B
) y  <->  E. z
( x B z  /\  z A y ) )
5 vex 2792 . . . . . . 7  |-  z  e. 
_V
63, 5brcnv 4863 . . . . . 6  |-  ( y `' A z  <->  z A
y )
75, 2brcnv 4863 . . . . . 6  |-  ( z `' B x  <->  x B
z )
86, 7anbi12i 678 . . . . 5  |-  ( ( y `' A z  /\  z `' B x )  <->  ( z A y  /\  x B z ) )
98exbii 1569 . . . 4  |-  ( E. z ( y `' A z  /\  z `' B x )  <->  E. z
( z A y  /\  x B z ) )
101, 4, 93bitr4i 268 . . 3  |-  ( x ( A  o.  B
) y  <->  E. z
( y `' A
z  /\  z `' B x ) )
1110opabbii 4084 . 2  |-  { <. y ,  x >.  |  x ( A  o.  B
) y }  =  { <. y ,  x >.  |  E. z ( y `' A z  /\  z `' B x ) }
12 df-cnv 4696 . 2  |-  `' ( A  o.  B )  =  { <. y ,  x >.  |  x
( A  o.  B
) y }
13 df-co 4697 . 2  |-  ( `' B  o.  `' A
)  =  { <. y ,  x >.  |  E. z ( y `' A z  /\  z `' B x ) }
1411, 12, 133eqtr4i 2314 1  |-  `' ( A  o.  B )  =  ( `' B  o.  `' A )
Colors of variables: wff set class
Syntax hints:    /\ wa 358   E.wex 1528    = wceq 1623   class class class wbr 4024   {copab 4077   `'ccnv 4687    o. ccom 4692
This theorem is referenced by:  rncoss  4944  rncoeq  4947  dmco  5179  cores2  5183  co01  5185  coi2  5187  relcnvtr  5190  dfdm2  5202  f1co  5412  cofunex2g  5702  fparlem3  6182  fparlem4  6183  suppfif1  7145  mapfien  7395  cnvps  14317  gimco  14728  gsumval3  15187  gsumzf1o  15192  cnco  16991  ptrescn  17329  qtopcn  17401  hmeoco  17459  cncombf  19009  deg1val  19478  cvmliftmolem1  23219  cvmlift2lem9a  23241  cvmlift2lem9  23249  relexpcnv  23436  trlcocnv  30188  tendoicl  30264  cdlemk45  30415
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pr 4213
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-rab 2553  df-v 2791  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-sn 3647  df-pr 3648  df-op 3650  df-br 4025  df-opab 4079  df-cnv 4696  df-co 4697
  Copyright terms: Public domain W3C validator