Metamath Proof Explorer

Theorem cnvco1

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

Ref Expression
Assertion cnvco1 
|- `' ( `' 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 
 |-  z e. _V
4 vex 
 |-  y e. _V
5 3 4 brcnv 
 |-  ( z `' B y <-> y B z )
6 5 bicomi 
 |-  ( y B z <-> z `' B y )
7 vex 
 |-  x e. _V
8 3 7 brcnv 
 |-  ( z `' A x <-> x A z )
9 6 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 7 4 opelcnv 
 |-  ( <. x , y >. e. `' ( `' A o. B ) <-> <. y , x >. e. ( `' A o. B ) )
12 4 7 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 7 4 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 )