Metamath Proof Explorer


Theorem cnvco2

Description: Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014)

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

Proof

Step Hyp Ref Expression
1 relcnv
 |-  Rel `' ( A o. `' B )
2 relco
 |-  Rel ( B o. `' A )
3 vex
 |-  y e. _V
4 vex
 |-  z e. _V
5 3 4 brcnv
 |-  ( y `' B z <-> z B y )
6 vex
 |-  x e. _V
7 6 4 brcnv
 |-  ( x `' A z <-> z A x )
8 7 bicomi
 |-  ( z A x <-> x `' A z )
9 5 8 anbi12ci
 |-  ( ( y `' B z /\ z A x ) <-> ( x `' A z /\ z B y ) )
10 9 exbii
 |-  ( E. z ( y `' B z /\ z A x ) <-> E. z ( x `' A z /\ z B y ) )
11 6 3 opelcnv
 |-  ( <. x , y >. e. `' ( A o. `' B ) <-> <. y , x >. e. ( A o. `' B ) )
12 3 6 opelco
 |-  ( <. y , x >. e. ( A o. `' B ) <-> E. z ( y `' B z /\ z A x ) )
13 11 12 bitri
 |-  ( <. x , y >. e. `' ( A o. `' B ) <-> E. z ( y `' B z /\ z A x ) )
14 6 3 opelco
 |-  ( <. x , y >. e. ( B o. `' A ) <-> E. z ( x `' A z /\ z B y ) )
15 10 13 14 3bitr4i
 |-  ( <. x , y >. e. `' ( A o. `' B ) <-> <. x , y >. e. ( B o. `' A ) )
16 1 2 15 eqrelriiv
 |-  `' ( A o. `' B ) = ( B o. `' A )