Metamath Proof Explorer

Theorem br1cossxrncnvssrres

Description: <. B , C >. and <. D , E >. are cosets by range Cartesian product with restricted converse subsets class: a binary relation. (Contributed by Peter Mazsa, 9-Jun-2021)

Ref Expression
Assertion br1cossxrncnvssrres 
|- ( ( ( B e. V /\ C e. W ) /\ ( D e. X /\ E e. Y ) ) -> ( <. B , C >. ,~ ( R |X. ( `' _S |` A ) ) <. D , E >. <-> E. u e. A ( ( C C_ u /\ u R B ) /\ ( E C_ u /\ u R D ) ) ) )

Proof

Step Hyp Ref Expression
1 br1cossxrnres 
 |-  ( ( ( B e. V /\ C e. W ) /\ ( D e. X /\ E e. Y ) ) -> ( <. B , C >. ,~ ( R |X. ( `' _S |` A ) ) <. D , E >. <-> E. u e. A ( ( u `' _S C /\ u R B ) /\ ( u `' _S E /\ u R D ) ) ) )
2 brcnvssr 
 |-  ( u e. _V -> ( u `' _S C <-> C C_ u ) )
3 2 elv 
 |-  ( u `' _S C <-> C C_ u )
4 3 anbi1i 
 |-  ( ( u `' _S C /\ u R B ) <-> ( C C_ u /\ u R B ) )
5 brcnvssr 
 |-  ( u e. _V -> ( u `' _S E <-> E C_ u ) )
6 5 elv 
 |-  ( u `' _S E <-> E C_ u )
7 6 anbi1i 
 |-  ( ( u `' _S E /\ u R D ) <-> ( E C_ u /\ u R D ) )
8 4 7 anbi12i 
 |-  ( ( ( u `' _S C /\ u R B ) /\ ( u `' _S E /\ u R D ) ) <-> ( ( C C_ u /\ u R B ) /\ ( E C_ u /\ u R D ) ) )
9 8 rexbii 
 |-  ( E. u e. A ( ( u `' _S C /\ u R B ) /\ ( u `' _S E /\ u R D ) ) <-> E. u e. A ( ( C C_ u /\ u R B ) /\ ( E C_ u /\ u R D ) ) )
10 1 9 bitrdi 
 |-  ( ( ( B e. V /\ C e. W ) /\ ( D e. X /\ E e. Y ) ) -> ( <. B , C >. ,~ ( R |X. ( `' _S |` A ) ) <. D , E >. <-> E. u e. A ( ( C C_ u /\ u R B ) /\ ( E C_ u /\ u R D ) ) ) )