Metamath Proof Explorer

Theorem cnvco

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)

Ref Expression
Assertion cnvco 
|- `' ( A o. B ) = ( `' B o. `' A )

Proof

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