Metamath Proof Explorer

Theorem br1cossinres

Description: B and C are cosets by an intersection with a restriction: a binary relation. (Contributed by Peter Mazsa, 31-Dec-2021)

Ref Expression
Assertion br1cossinres 
|- ( ( B e. V /\ C e. W ) -> ( B ,~ ( R i^i ( S |` A ) ) C <-> E. u e. A ( ( u S B /\ u R B ) /\ ( u S C /\ u R C ) ) ) )

Proof

Step Hyp Ref Expression
1 inres 
 |-  ( R i^i ( S |` A ) ) = ( ( R i^i S ) |` A )
2 1 cosseqi 
 |-  ,~ ( R i^i ( S |` A ) ) = ,~ ( ( R i^i S ) |` A )
3 2 breqi 
 |-  ( B ,~ ( R i^i ( S |` A ) ) C <-> B ,~ ( ( R i^i S ) |` A ) C )
4 br1cossres 
 |-  ( ( B e. V /\ C e. W ) -> ( B ,~ ( ( R i^i S ) |` A ) C <-> E. u e. A ( u ( R i^i S ) B /\ u ( R i^i S ) C ) ) )
5 brin 
 |-  ( u ( R i^i S ) B <-> ( u R B /\ u S B ) )
6 brin 
 |-  ( u ( R i^i S ) C <-> ( u R C /\ u S C ) )
7 5 6 anbi12i 
 |-  ( ( u ( R i^i S ) B /\ u ( R i^i S ) C ) <-> ( ( u R B /\ u S B ) /\ ( u R C /\ u S C ) ) )
8 an2anr 
 |-  ( ( ( u R B /\ u S B ) /\ ( u R C /\ u S C ) ) <-> ( ( u S B /\ u R B ) /\ ( u S C /\ u R C ) ) )
9 7 8 bitri 
 |-  ( ( u ( R i^i S ) B /\ u ( R i^i S ) C ) <-> ( ( u S B /\ u R B ) /\ ( u S C /\ u R C ) ) )
10 9 rexbii 
 |-  ( E. u e. A ( u ( R i^i S ) B /\ u ( R i^i S ) C ) <-> E. u e. A ( ( u S B /\ u R B ) /\ ( u S C /\ u R C ) ) )
11 4 10 bitrdi 
 |-  ( ( B e. V /\ C e. W ) -> ( B ,~ ( ( R i^i S ) |` A ) C <-> E. u e. A ( ( u S B /\ u R B ) /\ ( u S C /\ u R C ) ) ) )
12 3 11 syl5bb 
 |-  ( ( B e. V /\ C e. W ) -> ( B ,~ ( R i^i ( S |` A ) ) C <-> E. u e. A ( ( u S B /\ u R B ) /\ ( u S C /\ u R C ) ) ) )