eldisjdmqsim

Description: Shared output implies equal cosets (under ElDisj of quotient): if u and v both relate to the same x , then their cosets intersect, hence must coincide under quotient ElDisj . (Contributed by Peter Mazsa, 10-Feb-2026)

		Ref	Expression
	Assertion	eldisjdmqsim	$⊢ (ElDisj (dom R / R) \land R \in Rels) \to ((u R x \land v R x) \to [u] R = [v] R)$

Proof

Step	Hyp	Ref	Expression
1		elin	$⊢ x \in ([u] R \cap [v] R) \leftrightarrow (x \in [u] R \land x \in [v] R)$
2		elecALTV	$⊢ (u \in V \land x \in V) \to (x \in [u] R \leftrightarrow u R x)$
3	2	el2v	$⊢ x \in [u] R \leftrightarrow u R x$
4		elecALTV	$⊢ (v \in V \land x \in V) \to (x \in [v] R \leftrightarrow v R x)$
5	4	el2v	$⊢ x \in [v] R \leftrightarrow v R x$
6	3 5	anbi12i	$⊢ (x \in [u] R \land x \in [v] R) \leftrightarrow (u R x \land v R x)$
7	1 6	bitr2i	$⊢ (u R x \land v R x) \leftrightarrow x \in ([u] R \cap [v] R)$
8		ne0i	$⊢ x \in ([u] R \cap [v] R) \to [u] R \cap [v] R \neq \emptyset$
9	7 8	sylbi	$⊢ (u R x \land v R x) \to [u] R \cap [v] R \neq \emptyset$
10		19.8a	$⊢ u R x \to \exists x u R x$
11		eldmg	$⊢ u \in V \to (u \in dom R \leftrightarrow \exists x u R x)$
12	11	elv	$⊢ u \in dom R \leftrightarrow \exists x u R x$
13	10 12	sylibr	$⊢ u R x \to u \in dom R$
14		19.8a	$⊢ v R x \to \exists x v R x$
15		eldmg	$⊢ v \in V \to (v \in dom R \leftrightarrow \exists x v R x)$
16	15	elv	$⊢ v \in dom R \leftrightarrow \exists x v R x$
17	14 16	sylibr	$⊢ v R x \to v \in dom R$
18	13 17	anim12i	$⊢ (u R x \land v R x) \to (u \in dom R \land v \in dom R)$
19		eceldmqs	$⊢ R \in Rels \to ([u] R \in (dom R / R) \leftrightarrow u \in dom R)$
20		eceldmqs	$⊢ R \in Rels \to ([v] R \in (dom R / R) \leftrightarrow v \in dom R)$
21	19 20	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))$
22	18 21	imbitrrid	$⊢ R \in Rels \to ((u R x \land v R x) \to ([u] R \in (dom R / R) \land [v] R \in (dom R / R)))$
23	22	adantl	$⊢ (ElDisj (dom R / R) \land R \in Rels) \to ((u R x \land v R x) \to ([u] R \in (dom R / R) \land [v] R \in (dom R / R)))$
24		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))$
25	24	adantr	$⊢ (ElDisj (dom R / R) \land 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))$
26	23 25	syld	$⊢ (ElDisj (dom R / R) \land R \in Rels) \to ((u R x \land v R x) \to ([u] R \cap [v] R \neq \emptyset \to [u] R = [v] R))$
27	9 26	mpdi	$⊢ (ElDisj (dom R / R) \land R \in Rels) \to ((u R x \land v R x) \to [u] R = [v] R)$

Metamath Proof Explorer

Theorem eldisjdmqsim

Proof