This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eleccossin

Description: Two ways of saying that the coset of A and the coset of C have the common element B . (Contributed by Peter Mazsa, 15-Oct-2021)

Ref Expression
Assertion eleccossin 
|- ( ( B e. V /\ C e. W ) -> ( B e. ( [ A ] ,~ R i^i [ C ] ,~ R ) <-> ( A ,~ R B /\ B ,~ R C ) ) )

Proof

Step Hyp Ref Expression
1 elin 
 |-  ( B e. ( [ A ] ,~ R i^i [ C ] ,~ R ) <-> ( B e. [ A ] ,~ R /\ B e. [ C ] ,~ R ) )
2 relcoss 
 |-  Rel ,~ R
3 relelec 
 |-  ( Rel ,~ R -> ( B e. [ A ] ,~ R <-> A ,~ R B ) )
4 2 3 ax-mp 
 |-  ( B e. [ A ] ,~ R <-> A ,~ R B )
5 relelec 
 |-  ( Rel ,~ R -> ( B e. [ C ] ,~ R <-> C ,~ R B ) )
6 2 5 ax-mp 
 |-  ( B e. [ C ] ,~ R <-> C ,~ R B )
7 4 6 anbi12i 
 |-  ( ( B e. [ A ] ,~ R /\ B e. [ C ] ,~ R ) <-> ( A ,~ R B /\ C ,~ R B ) )
8 1 7 bitri 
 |-  ( B e. ( [ A ] ,~ R i^i [ C ] ,~ R ) <-> ( A ,~ R B /\ C ,~ R B ) )
9 brcosscnvcoss 
 |-  ( ( B e. V /\ C e. W ) -> ( B ,~ R C <-> C ,~ R B ) )
10 9 anbi2d 
 |-  ( ( B e. V /\ C e. W ) -> ( ( A ,~ R B /\ B ,~ R C ) <-> ( A ,~ R B /\ C ,~ R B ) ) )
11 8 10 bitr4id 
 |-  ( ( B e. V /\ C e. W ) -> ( B e. ( [ A ] ,~ R i^i [ C ] ,~ R ) <-> ( A ,~ R B /\ B ,~ R C ) ) )