disjecxrn

Description: Two ways of saying that ( R |X. S ) -cosets are disjoint. (Contributed by Peter Mazsa, 19-Jun-2020) (Revised by Peter Mazsa, 21-Aug-2023)

		Ref	Expression
	Assertion	disjecxrn	$⊢ (A \in V \land B \in W) \to ([A] R ⋉ S \cap [B] R ⋉ S = \emptyset \leftrightarrow ([A] R \cap [B] R = \emptyset \lor [A] S \cap [B] S = \emptyset))$

Proof

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

Metamath Proof Explorer

Theorem disjecxrn

Proof