Metamath Proof Explorer

Theorem eldisjdmqsim2

Description: ElDisj of quotient implies coset-disjointness (domain form). Converts element-disjointness of the quotient carrier into a usable "cosets don't overlap unless equal" rule. (Contributed by Peter Mazsa, 10-Feb-2026)

		Ref	Expression
	Assertion	eldisjdmqsim2	$⊢ (ElDisj (dom R / R) \land R \in Rels) \to ((u \in dom R \land v \in dom R) \to ([u] R \cap [v] R \neq \emptyset \to [u] R = [v] R))$

Proof

Step	Hyp	Ref	Expression
1		eldisjim3	$⊢ ElDisj (dom R / R) \to (([u] R \in (dom R / R) \land [v] R \in (dom R / R)) \to ([u] R \cap [v] R \neq \emptyset \to [u] R = [v] R))$
2		eceldmqs	$⊢ R \in Rels \to ([u] R \in (dom R / R) \leftrightarrow u \in dom R)$
3		eceldmqs	$⊢ R \in Rels \to ([v] R \in (dom R / R) \leftrightarrow v \in dom R)$
4	2 3	anbi12d	$⊢ R \in Rels \to (([u] R \in (dom R / R) \land [v] R \in (dom R / R)) \leftrightarrow (u \in dom R \land v \in dom R))$
5	4	imbi1d	$⊢ R \in Rels \to ((([u] R \in (dom R / R) \land [v] R \in (dom R / R)) \to ([u] R \cap [v] R \neq \emptyset \to [u] R = [v] R)) \leftrightarrow ((u \in dom R \land v \in dom R) \to ([u] R \cap [v] R \neq \emptyset \to [u] R = [v] R)))$
6	1 5	imbitrid	$⊢ R \in Rels \to (ElDisj (dom R / R) \to ((u \in dom R \land v \in dom R) \to ([u] R \cap [v] R \neq \emptyset \to [u] R = [v] R)))$
7	6	impcom	$⊢ (ElDisj (dom R / R) \land R \in Rels) \to ((u \in dom R \land v \in dom R) \to ([u] R \cap [v] R \neq \emptyset \to [u] R = [v] R))$