br2coss

Description: Cosets by ,R binary relation. (Contributed by Peter Mazsa, 25-Aug-2019)

		Ref	Expression
	Assertion	br2coss	$⊢ (A \in V \land B \in W) \to (A ≀ ≀ R B \leftrightarrow [A] ≀ R \cap [B] ≀ R \neq \emptyset)$

Step	Hyp	Ref	Expression
1		brcoss3	$⊢ (A \in V \land B \in W) \to (A ≀ ≀ R B \leftrightarrow [A] {≀ R}^{-1} \cap [B] {≀ R}^{-1} \neq \emptyset)$
2		cnvcosseq	$⊢ {≀ R}^{-1} = ≀ R$
3	2	eceq2i	$⊢ [A] {≀ R}^{-1} = [A] ≀ R$
4	2	eceq2i	$⊢ [B] {≀ R}^{-1} = [B] ≀ R$
5	3 4	ineq12i	$⊢ [A] {≀ R}^{-1} \cap [B] {≀ R}^{-1} = [A] ≀ R \cap [B] ≀ R$
6	5	neeq1i	$⊢ [A] {≀ R}^{-1} \cap [B] {≀ R}^{-1} \neq \emptyset \leftrightarrow [A] ≀ R \cap [B] ≀ R \neq \emptyset$
7	1 6	bitrdi	$⊢ (A \in V \land B \in W) \to (A ≀ ≀ R B \leftrightarrow [A] ≀ R \cap [B] ≀ R \neq \emptyset)$

Metamath Proof Explorer