brcoss3

Description: Alternate form of the A and B are cosets by R binary relation. (Contributed by Peter Mazsa, 26-Mar-2019)

		Ref	Expression
	Assertion	brcoss3	$⊢ (A \in V \land B \in W) \to (A ≀ R B \leftrightarrow [A] R^{-1} \cap [B] R^{-1} \neq \emptyset)$

Step	Hyp	Ref	Expression
1		brcnvg	$⊢ (A \in V \land u \in V) \to (A R^{-1} u \leftrightarrow u R A)$
2	1	elvd	$⊢ A \in V \to (A R^{-1} u \leftrightarrow u R A)$
3		brcnvg	$⊢ (B \in W \land u \in V) \to (B R^{-1} u \leftrightarrow u R B)$
4	3	elvd	$⊢ B \in W \to (B R^{-1} u \leftrightarrow u R B)$
5	2 4	bi2anan9	$⊢ (A \in V \land B \in W) \to ((A R^{-1} u \land B R^{-1} u) \leftrightarrow (u R A \land u R B))$
6	5	exbidv	$⊢ (A \in V \land B \in W) \to (\exists u (A R^{-1} u \land B R^{-1} u) \leftrightarrow \exists u (u R A \land u R B))$
7		ecinn0	$⊢ (A \in V \land B \in W) \to ([A] R^{-1} \cap [B] R^{-1} \neq \emptyset \leftrightarrow \exists u (A R^{-1} u \land B R^{-1} u))$
8		brcoss	$⊢ (A \in V \land B \in W) \to (A ≀ R B \leftrightarrow \exists u (u R A \land u R B))$
9	6 7 8	3bitr4rd	$⊢ (A \in V \land B \in W) \to (A ≀ R B \leftrightarrow [A] R^{-1} \cap [B] R^{-1} \neq \emptyset)$

Metamath Proof Explorer