Metamath Proof Explorer

Theorem br1cossxrnres

Description: <. B , C >. and <. D , E >. are cosets by an intersection with a restriction: a binary relation. (Contributed by Peter Mazsa, 8-Jun-2021)

Ref Expression
Assertion 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 ) ) ) )

Proof

Step Hyp Ref Expression
1 xrnres2 
 |-  ( ( R |X. S ) |` A ) = ( R |X. ( S |` A ) )
2 1 cosseqi 
 |-  ,~ ( ( R |X. S ) |` A ) = ,~ ( R |X. ( S |` A ) )
3 2 breqi 
 |-  ( <. B , C >. ,~ ( ( R |X. S ) |` A ) <. D , E >. <-> <. B , C >. ,~ ( R |X. ( S |` A ) ) <. D , E >. )
4 opex 
 |-  <. B , C >. e. _V
5 opex 
 |-  <. D , E >. e. _V
6 br1cossres 
 |-  ( ( <. B , C >. e. _V /\ <. D , E >. e. _V ) -> ( <. B , C >. ,~ ( ( R |X. S ) |` A ) <. D , E >. <-> E. u e. A ( u ( R |X. S ) <. B , C >. /\ u ( R |X. S ) <. D , E >. ) ) )
7 4 5 6 mp2an 
 |-  ( <. B , C >. ,~ ( ( R |X. S ) |` A ) <. D , E >. <-> E. u e. A ( u ( R |X. S ) <. B , C >. /\ u ( R |X. S ) <. D , E >. ) )
8 brxrn 
 |-  ( ( u e. _V /\ B e. V /\ C e. W ) -> ( u ( R |X. S ) <. B , C >. <-> ( u R B /\ u S C ) ) )
9 8 el3v1 
 |-  ( ( B e. V /\ C e. W ) -> ( u ( R |X. S ) <. B , C >. <-> ( u R B /\ u S C ) ) )
10 brxrn 
 |-  ( ( u e. _V /\ D e. X /\ E e. Y ) -> ( u ( R |X. S ) <. D , E >. <-> ( u R D /\ u S E ) ) )
11 10 el3v1 
 |-  ( ( D e. X /\ E e. Y ) -> ( u ( R |X. S ) <. D , E >. <-> ( u R D /\ u S E ) ) )
12 9 11 bi2anan9 
 |-  ( ( ( B e. V /\ C e. W ) /\ ( D e. X /\ E e. Y ) ) -> ( ( u ( R |X. S ) <. B , C >. /\ u ( R |X. S ) <. D , E >. ) <-> ( ( u R B /\ u S C ) /\ ( u R D /\ u S E ) ) ) )
13 an2anr 
 |-  ( ( ( u R B /\ u S C ) /\ ( u R D /\ u S E ) ) <-> ( ( u S C /\ u R B ) /\ ( u S E /\ u R D ) ) )
14 12 13 bitrdi 
 |-  ( ( ( B e. V /\ C e. W ) /\ ( D e. X /\ E e. Y ) ) -> ( ( u ( R |X. S ) <. B , C >. /\ u ( R |X. S ) <. D , E >. ) <-> ( ( u S C /\ u R B ) /\ ( u S E /\ u R D ) ) ) )
15 14 rexbidv 
 |-  ( ( ( B e. V /\ C e. W ) /\ ( D e. X /\ E e. Y ) ) -> ( E. u e. A ( u ( R |X. S ) <. B , C >. /\ u ( R |X. S ) <. D , E >. ) <-> E. u e. A ( ( u S C /\ u R B ) /\ ( u S E /\ u R D ) ) ) )
16 7 15 syl5bb 
 |-  ( ( ( 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 ) ) ) )
17 3 16 bitr3id 
 |-  ( ( ( 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 ) ) ) )