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 ) ) )