Metamath Proof Explorer

Theorem br1cosscnvxrn

Description: A and B are cosets by the converse range Cartesian product: a binary relation. (Contributed by Peter Mazsa, 19-Apr-2020) (Revised by Peter Mazsa, 21-Sep-2021)

Ref Expression
Assertion br1cosscnvxrn 
|- ( ( A e. V /\ B e. W ) -> ( A ,~ `' ( R |X. S ) B <-> ( A ,~ `' R B /\ A ,~ `' S B ) ) )

Proof

Step Hyp Ref Expression
1 ecxrn 
 |-  ( A e. V -> [ A ] ( R |X. S ) = { <. x , y >. | ( A R x /\ A S y ) } )
2 ecxrn 
 |-  ( B e. W -> [ B ] ( R |X. S ) = { <. x , y >. | ( B R x /\ B S y ) } )
3 1 2 ineqan12d 
 |-  ( ( A e. V /\ B e. W ) -> ( [ A ] ( R |X. S ) i^i [ B ] ( R |X. S ) ) = ( { <. x , y >. | ( A R x /\ A S y ) } i^i { <. x , y >. | ( B R x /\ B S y ) } ) )
4 inopab 
 |-  ( { <. x , y >. | ( A R x /\ A S y ) } i^i { <. x , y >. | ( B R x /\ B S y ) } ) = { <. x , y >. | ( ( A R x /\ A S y ) /\ ( B R x /\ B S y ) ) }
5 3 4 eqtrdi 
 |-  ( ( A e. V /\ B e. W ) -> ( [ A ] ( R |X. S ) i^i [ B ] ( R |X. S ) ) = { <. x , y >. | ( ( A R x /\ A S y ) /\ ( B R x /\ B S y ) ) } )
6 an4 
 |-  ( ( ( A R x /\ A S y ) /\ ( B R x /\ B S y ) ) <-> ( ( A R x /\ B R x ) /\ ( A S y /\ B S y ) ) )
7 6 opabbii 
 |-  { <. x , y >. | ( ( A R x /\ A S y ) /\ ( B R x /\ B S y ) ) } = { <. x , y >. | ( ( A R x /\ B R x ) /\ ( A S y /\ B S y ) ) }
8 5 7 eqtrdi 
 |-  ( ( A e. V /\ B e. W ) -> ( [ A ] ( R |X. S ) i^i [ B ] ( R |X. S ) ) = { <. x , y >. | ( ( A R x /\ B R x ) /\ ( A S y /\ B S y ) ) } )
9 8 neeq1d 
 |-  ( ( A e. V /\ B e. W ) -> ( ( [ A ] ( R |X. S ) i^i [ B ] ( R |X. S ) ) =/= (/) <-> { <. x , y >. | ( ( A R x /\ B R x ) /\ ( A S y /\ B S y ) ) } =/= (/) ) )
10 opabn0 
 |-  ( { <. x , y >. | ( ( A R x /\ B R x ) /\ ( A S y /\ B S y ) ) } =/= (/) <-> E. x E. y ( ( A R x /\ B R x ) /\ ( A S y /\ B S y ) ) )
11 exdistrv 
 |-  ( E. x E. y ( ( A R x /\ B R x ) /\ ( A S y /\ B S y ) ) <-> ( E. x ( A R x /\ B R x ) /\ E. y ( A S y /\ B S y ) ) )
12 10 11 bitri 
 |-  ( { <. x , y >. | ( ( A R x /\ B R x ) /\ ( A S y /\ B S y ) ) } =/= (/) <-> ( E. x ( A R x /\ B R x ) /\ E. y ( A S y /\ B S y ) ) )
13 9 12 bitrdi 
 |-  ( ( A e. V /\ B e. W ) -> ( ( [ A ] ( R |X. S ) i^i [ B ] ( R |X. S ) ) =/= (/) <-> ( E. x ( A R x /\ B R x ) /\ E. y ( A S y /\ B S y ) ) ) )
14 brcosscnv2 
 |-  ( ( A e. V /\ B e. W ) -> ( A ,~ `' ( R |X. S ) B <-> ( [ A ] ( R |X. S ) i^i [ B ] ( R |X. S ) ) =/= (/) ) )
15 brcosscnv 
 |-  ( ( A e. V /\ B e. W ) -> ( A ,~ `' R B <-> E. x ( A R x /\ B R x ) ) )
16 brcosscnv 
 |-  ( ( A e. V /\ B e. W ) -> ( A ,~ `' S B <-> E. y ( A S y /\ B S y ) ) )
17 15 16 anbi12d 
 |-  ( ( A e. V /\ B e. W ) -> ( ( A ,~ `' R B /\ A ,~ `' S B ) <-> ( E. x ( A R x /\ B R x ) /\ E. y ( A S y /\ B S y ) ) ) )
18 13 14 17 3bitr4d 
 |-  ( ( A e. V /\ B e. W ) -> ( A ,~ `' ( R |X. S ) B <-> ( A ,~ `' R B /\ A ,~ `' S B ) ) )