Metamath Proof Explorer

Theorem br1cosscnvxrn

Description: A and B are cosets by the converse range Cartesian product: a binary relation. (Contributed by Peter Mazsa, 19-Apr-2020) (Revised by Peter Mazsa, 21-Sep-2021)

		Ref	Expression
	Assertion	br1cosscnvxrn	$⊢ (A \in V \land B \in W) \to (A ≀ {R ⋉ S}^{-1} B \leftrightarrow (A ≀ R^{-1} B \land A ≀ S^{-1} B))$

Proof

Step	Hyp	Ref	Expression
1		ecxrn	$⊢ A \in V \to [A] R ⋉ S = \{⟨x, y⟩ \| (A R x \land A S y)\}$
2		ecxrn	$⊢ B \in W \to [B] R ⋉ S = \{⟨x, y⟩ \| (B R x \land B S y)\}$
3	1 2	ineqan12d	$⊢ (A \in V \land B \in W) \to [A] R ⋉ S \cap [B] R ⋉ S = \{⟨x, y⟩ \| (A R x \land A S y)\} \cap \{⟨x, y⟩ \| (B R x \land B S y)\}$
4		inopab	$⊢ \{⟨x, y⟩ \| (A R x \land A S y)\} \cap \{⟨x, y⟩ \| (B R x \land B S y)\} = \{⟨x, y⟩ \| ((A R x \land A S y) \land (B R x \land B S y))\}$
5	3 4	eqtrdi	$⊢ (A \in V \land B \in W) \to [A] R ⋉ S \cap [B] R ⋉ S = \{⟨x, y⟩ \| ((A R x \land A S y) \land (B R x \land B S y))\}$
6		an4	$⊢ ((A R x \land A S y) \land (B R x \land B S y)) \leftrightarrow ((A R x \land B R x) \land (A S y \land B S y))$
7	6	opabbii	$⊢ \{⟨x, y⟩ \| ((A R x \land A S y) \land (B R x \land B S y))\} = \{⟨x, y⟩ \| ((A R x \land B R x) \land (A S y \land B S y))\}$
8	5 7	eqtrdi	$⊢ (A \in V \land B \in W) \to [A] R ⋉ S \cap [B] R ⋉ S = \{⟨x, y⟩ \| ((A R x \land B R x) \land (A S y \land B S y))\}$
9	8	neeq1d	$⊢ (A \in V \land B \in W) \to ([A] R ⋉ S \cap [B] R ⋉ S \neq \emptyset \leftrightarrow \{⟨x, y⟩ \| ((A R x \land B R x) \land (A S y \land B S y))\} \neq \emptyset)$
10		opabn0	$⊢ \{⟨x, y⟩ \| ((A R x \land B R x) \land (A S y \land B S y))\} \neq \emptyset \leftrightarrow \exists x \exists y ((A R x \land B R x) \land (A S y \land B S y))$
11		exdistrv	$⊢ \exists x \exists y ((A R x \land B R x) \land (A S y \land B S y)) \leftrightarrow (\exists x (A R x \land B R x) \land \exists y (A S y \land B S y))$
12	10 11	bitri	$⊢ \{⟨x, y⟩ \| ((A R x \land B R x) \land (A S y \land B S y))\} \neq \emptyset \leftrightarrow (\exists x (A R x \land B R x) \land \exists y (A S y \land B S y))$
13	9 12	bitrdi	$⊢ (A \in V \land B \in W) \to ([A] R ⋉ S \cap [B] R ⋉ S \neq \emptyset \leftrightarrow (\exists x (A R x \land B R x) \land \exists y (A S y \land B S y)))$
14		brcosscnv2	$⊢ (A \in V \land B \in W) \to (A ≀ {R ⋉ S}^{-1} B \leftrightarrow [A] R ⋉ S \cap [B] R ⋉ S \neq \emptyset)$
15		brcosscnv	$⊢ (A \in V \land B \in W) \to (A ≀ R^{-1} B \leftrightarrow \exists x (A R x \land B R x))$
16		brcosscnv	$⊢ (A \in V \land B \in W) \to (A ≀ S^{-1} B \leftrightarrow \exists y (A S y \land B S y))$
17	15 16	anbi12d	$⊢ (A \in V \land B \in W) \to ((A ≀ R^{-1} B \land A ≀ S^{-1} B) \leftrightarrow (\exists x (A R x \land B R x) \land \exists y (A S y \land B S y)))$
18	13 14 17	3bitr4d	$⊢ (A \in V \land B \in W) \to (A ≀ {R ⋉ S}^{-1} B \leftrightarrow (A ≀ R^{-1} B \land A ≀ S^{-1} B))$