brcosscnv

Description: A and B are cosets by converse R : a binary relation. (Contributed by Peter Mazsa, 23-Jan-2019)

		Ref	Expression
	Assertion	brcosscnv	$⊢ (A \in V \land B \in W) \to (A ≀ R^{-1} B \leftrightarrow \exists x (A R x \land B R x))$

Step	Hyp	Ref	Expression
1		brcoss	$⊢ (A \in V \land B \in W) \to (A ≀ R^{-1} B \leftrightarrow \exists x (x R^{-1} A \land x R^{-1} B))$
2		brcnvg	$⊢ (x \in V \land A \in V) \to (x R^{-1} A \leftrightarrow A R x)$
3	2	el2v1	$⊢ A \in V \to (x R^{-1} A \leftrightarrow A R x)$
4		brcnvg	$⊢ (x \in V \land B \in W) \to (x R^{-1} B \leftrightarrow B R x)$
5	4	el2v1	$⊢ B \in W \to (x R^{-1} B \leftrightarrow B R x)$
6	3 5	bi2anan9	$⊢ (A \in V \land B \in W) \to ((x R^{-1} A \land x R^{-1} B) \leftrightarrow (A R x \land B R x))$
7	6	exbidv	$⊢ (A \in V \land B \in W) \to (\exists x (x R^{-1} A \land x R^{-1} B) \leftrightarrow \exists x (A R x \land B R x))$
8	1 7	bitrd	$⊢ (A \in V \land B \in W) \to (A ≀ R^{-1} B \leftrightarrow \exists x (A R x \land B R x))$

Metamath Proof Explorer