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 )