disjimeceqim

Description: Disj implies coset-equality injectivity (domain-wise). Extracts the practical consequence of Disj : the map u |-> [ u ] R is injective on dom R . This is exactly the "canonicity" property used repeatedly when turning E* into E! and when reasoning about uniqueness of representatives. (Contributed by Peter Mazsa, 3-Feb-2026)

		Ref	Expression
	Assertion	disjimeceqim	$⊢ Disj R \to \forall u \in dom R \forall v \in dom R ([u] R = [v] R \to u = v)$

Proof

Step	Hyp	Ref	Expression
1		ecdmn0	$⊢ u \in dom R \leftrightarrow [u] R \neq \emptyset$
2	1	biimpi	$⊢ u \in dom R \to [u] R \neq \emptyset$
3		ineq2	$⊢ [u] R = [v] R \to [u] R \cap [u] R = [u] R \cap [v] R$
4		inidm	$⊢ [u] R \cap [u] R = [u] R$
5	3 4	eqtr3di	$⊢ [u] R = [v] R \to [u] R \cap [v] R = [u] R$
6	5	neeq1d	$⊢ [u] R = [v] R \to ([u] R \cap [v] R \neq \emptyset \leftrightarrow [u] R \neq \emptyset)$
7	2 6	syl5ibrcom	$⊢ u \in dom R \to ([u] R = [v] R \to [u] R \cap [v] R \neq \emptyset)$
8	7	rgen	$⊢ \forall u \in dom R ([u] R = [v] R \to [u] R \cap [v] R \neq \emptyset)$
9	8	rgenw	$⊢ \forall v \in dom R \forall u \in dom R ([u] R = [v] R \to [u] R \cap [v] R \neq \emptyset)$
10		ralcom	$⊢ \forall v \in dom R \forall u \in dom R ([u] R = [v] R \to [u] R \cap [v] R \neq \emptyset) \leftrightarrow \forall u \in dom R \forall v \in dom R ([u] R = [v] R \to [u] R \cap [v] R \neq \emptyset)$
11	9 10	mpbi	$⊢ \forall u \in dom R \forall v \in dom R ([u] R = [v] R \to [u] R \cap [v] R \neq \emptyset)$
12		dfdisjALTV5a	$⊢ Disj R \leftrightarrow (\forall u \in dom R \forall v \in dom R ([u] R \cap [v] R \neq \emptyset \to u = v) \land Rel R)$
13	12	simplbi	$⊢ Disj R \to \forall u \in dom R \forall v \in dom R ([u] R \cap [v] R \neq \emptyset \to u = v)$
14		r19.26-2	$⊢ \forall u \in dom R \forall v \in dom R (([u] R = [v] R \to [u] R \cap [v] R \neq \emptyset) \land ([u] R \cap [v] R \neq \emptyset \to u = v)) \leftrightarrow (\forall u \in dom R \forall v \in dom R ([u] R = [v] R \to [u] R \cap [v] R \neq \emptyset) \land \forall u \in dom R \forall v \in dom R ([u] R \cap [v] R \neq \emptyset \to u = v))$
15		pm3.33	$⊢ (([u] R = [v] R \to [u] R \cap [v] R \neq \emptyset) \land ([u] R \cap [v] R \neq \emptyset \to u = v)) \to ([u] R = [v] R \to u = v)$
16	15	2ralimi	$⊢ \forall u \in dom R \forall v \in dom R (([u] R = [v] R \to [u] R \cap [v] R \neq \emptyset) \land ([u] R \cap [v] R \neq \emptyset \to u = v)) \to \forall u \in dom R \forall v \in dom R ([u] R = [v] R \to u = v)$
17	14 16	sylbir	$⊢ (\forall u \in dom R \forall v \in dom R ([u] R = [v] R \to [u] R \cap [v] R \neq \emptyset) \land \forall u \in dom R \forall v \in dom R ([u] R \cap [v] R \neq \emptyset \to u = v)) \to \forall u \in dom R \forall v \in dom R ([u] R = [v] R \to u = v)$
18	11 13 17	sylancr	$⊢ Disj R \to \forall u \in dom R \forall v \in dom R ([u] R = [v] R \to u = v)$

Metamath Proof Explorer

Theorem disjimeceqim

Proof