This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnviin

Description: The converse of an intersection is the intersection of the converse. (Contributed by FL, 15-Oct-2012)

Ref Expression
Assertion cnviin 
|- ( A =/= (/) -> `' |^|_ x e. A B = |^|_ x e. A `' B )

Proof

Step Hyp Ref Expression
1 relcnv 
 |-  Rel `' |^|_ x e. A B
2 relcnv 
 |-  Rel `' B
3 df-rel 
 |-  ( Rel `' B <-> `' B C_ ( _V X. _V ) )
4 2 3 mpbi 
 |-  `' B C_ ( _V X. _V )
5 4 rgenw 
 |-  A. x e. A `' B C_ ( _V X. _V )
6 r19.2z 
 |-  ( ( A =/= (/) /\ A. x e. A `' B C_ ( _V X. _V ) ) -> E. x e. A `' B C_ ( _V X. _V ) )
7 5 6 mpan2 
 |-  ( A =/= (/) -> E. x e. A `' B C_ ( _V X. _V ) )
8 iinss 
 |-  ( E. x e. A `' B C_ ( _V X. _V ) -> |^|_ x e. A `' B C_ ( _V X. _V ) )
9 7 8 syl 
 |-  ( A =/= (/) -> |^|_ x e. A `' B C_ ( _V X. _V ) )
10 df-rel 
 |-  ( Rel |^|_ x e. A `' B <-> |^|_ x e. A `' B C_ ( _V X. _V ) )
11 9 10 sylibr 
 |-  ( A =/= (/) -> Rel |^|_ x e. A `' B )
12 opex 
 |-  <. b , a >. e. _V
13 eliin 
 |-  ( <. b , a >. e. _V -> ( <. b , a >. e. |^|_ x e. A B <-> A. x e. A <. b , a >. e. B ) )
14 12 13 ax-mp 
 |-  ( <. b , a >. e. |^|_ x e. A B <-> A. x e. A <. b , a >. e. B )
15 vex 
 |-  a e. _V
16 vex 
 |-  b e. _V
17 15 16 opelcnv 
 |-  ( <. a , b >. e. `' |^|_ x e. A B <-> <. b , a >. e. |^|_ x e. A B )
18 opex 
 |-  <. a , b >. e. _V
19 eliin 
 |-  ( <. a , b >. e. _V -> ( <. a , b >. e. |^|_ x e. A `' B <-> A. x e. A <. a , b >. e. `' B ) )
20 18 19 ax-mp 
 |-  ( <. a , b >. e. |^|_ x e. A `' B <-> A. x e. A <. a , b >. e. `' B )
21 15 16 opelcnv 
 |-  ( <. a , b >. e. `' B <-> <. b , a >. e. B )
22 21 ralbii 
 |-  ( A. x e. A <. a , b >. e. `' B <-> A. x e. A <. b , a >. e. B )
23 20 22 bitri 
 |-  ( <. a , b >. e. |^|_ x e. A `' B <-> A. x e. A <. b , a >. e. B )
24 14 17 23 3bitr4i 
 |-  ( <. a , b >. e. `' |^|_ x e. A B <-> <. a , b >. e. |^|_ x e. A `' B )
25 24 eqrelriv 
 |-  ( ( Rel `' |^|_ x e. A B /\ Rel |^|_ x e. A `' B ) -> `' |^|_ x e. A B = |^|_ x e. A `' B )
26 1 11 25 sylancr 
 |-  ( A =/= (/) -> `' |^|_ x e. A B = |^|_ x e. A `' B )