Metamath Proof Explorer

Theorem disjecxrncnvep

Description: Two ways of saying that cosets are disjoint, special case of disjecxrn . (Contributed by Peter Mazsa, 12-Jul-2020) (Revised by Peter Mazsa, 25-Aug-2023)

		Ref	Expression
	Assertion	disjecxrncnvep	$⊢ (A \in V \land B \in W) \to ([A] R ⋉ E^{-1} \cap [B] R ⋉ E^{-1} = \emptyset \leftrightarrow (A \cap B = \emptyset \lor [A] R \cap [B] R = \emptyset))$

Proof

Step	Hyp	Ref	Expression
1		disjecxrn	$⊢ (A \in V \land B \in W) \to ([A] R ⋉ E^{-1} \cap [B] R ⋉ E^{-1} = \emptyset \leftrightarrow ([A] R \cap [B] R = \emptyset \lor [A] E^{-1} \cap [B] E^{-1} = \emptyset))$
2		orcom	$⊢ ([A] R \cap [B] R = \emptyset \lor [A] E^{-1} \cap [B] E^{-1} = \emptyset) \leftrightarrow ([A] E^{-1} \cap [B] E^{-1} = \emptyset \lor [A] R \cap [B] R = \emptyset)$
3	1 2	bitrdi	$⊢ (A \in V \land B \in W) \to ([A] R ⋉ E^{-1} \cap [B] R ⋉ E^{-1} = \emptyset \leftrightarrow ([A] E^{-1} \cap [B] E^{-1} = \emptyset \lor [A] R \cap [B] R = \emptyset))$
4		disjeccnvep	$⊢ (A \in V \land B \in W) \to ([A] E^{-1} \cap [B] E^{-1} = \emptyset \leftrightarrow A \cap B = \emptyset)$
5	4	orbi1d	$⊢ (A \in V \land B \in W) \to (([A] E^{-1} \cap [B] E^{-1} = \emptyset \lor [A] R \cap [B] R = \emptyset) \leftrightarrow (A \cap B = \emptyset \lor [A] R \cap [B] R = \emptyset))$
6	3 5	bitrd	$⊢ (A \in V \land B \in W) \to ([A] R ⋉ E^{-1} \cap [B] R ⋉ E^{-1} = \emptyset \leftrightarrow (A \cap B = \emptyset \lor [A] R \cap [B] R = \emptyset))$