Metamath Proof Explorer

Theorem relbrcoss

Description: A and B are cosets by relation R : a binary relation. (Contributed by Peter Mazsa, 22-Apr-2021)

Ref Expression
Assertion relbrcoss 
|- ( ( A e. V /\ B e. W ) -> ( Rel R -> ( A ,~ R B <-> E. x e. dom R ( A e. [ x ] R /\ B e. [ x ] R ) ) ) )

Proof

Step Hyp Ref Expression
1 resdm 
 |-  ( Rel R -> ( R |` dom R ) = R )
2 1 cosseqd 
 |-  ( Rel R -> ,~ ( R |` dom R ) = ,~ R )
3 2 breqd 
 |-  ( Rel R -> ( A ,~ ( R |` dom R ) B <-> A ,~ R B ) )
4 3 adantl 
 |-  ( ( ( A e. V /\ B e. W ) /\ Rel R ) -> ( A ,~ ( R |` dom R ) B <-> A ,~ R B ) )
5 br1cossres2 
 |-  ( ( A e. V /\ B e. W ) -> ( A ,~ ( R |` dom R ) B <-> E. x e. dom R ( A e. [ x ] R /\ B e. [ x ] R ) ) )
6 5 adantr 
 |-  ( ( ( A e. V /\ B e. W ) /\ Rel R ) -> ( A ,~ ( R |` dom R ) B <-> E. x e. dom R ( A e. [ x ] R /\ B e. [ x ] R ) ) )
7 4 6 bitr3d 
 |-  ( ( ( A e. V /\ B e. W ) /\ Rel R ) -> ( A ,~ R B <-> E. x e. dom R ( A e. [ x ] R /\ B e. [ x ] R ) ) )
8 7 ex 
 |-  ( ( A e. V /\ B e. W ) -> ( Rel R -> ( A ,~ R B <-> E. x e. dom R ( A e. [ x ] R /\ B e. [ x ] R ) ) ) )