Theorem 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 -> A. u e. dom R A. v e. dom R ( [ u ] R = [ v ] R -> u = v ) )

Proof

Step	Hyp	Ref	Expression
1		ecdmn0	|- ( u e. dom R <-> [ u ] R =/= (/) )
2	1	biimpi	|- ( u e. dom R -> [ u ] R =/= (/) )
3		ineq2	|- ( [ u ] R = [ v ] R -> ( [ u ] R i^i [ u ] R ) = ( [ u ] R i^i [ v ] R ) )
4		inidm	|- ( [ u ] R i^i [ u ] R ) = [ u ] R
5	3 4	eqtr3di	|- ( [ u ] R = [ v ] R -> ( [ u ] R i^i [ v ] R ) = [ u ] R )
6	5	neeq1d	|- ( [ u ] R = [ v ] R -> ( ( [ u ] R i^i [ v ] R ) =/= (/) <-> [ u ] R =/= (/) ) )
7	2 6	syl5ibrcom	|- ( u e. dom R -> ( [ u ] R = [ v ] R -> ( [ u ] R i^i [ v ] R ) =/= (/) ) )
8	7	rgen	|- A. u e. dom R ( [ u ] R = [ v ] R -> ( [ u ] R i^i [ v ] R ) =/= (/) )
9	8	rgenw	|- A. v e. dom R A. u e. dom R ( [ u ] R = [ v ] R -> ( [ u ] R i^i [ v ] R ) =/= (/) )
10		ralcom	|- ( A. v e. dom R A. u e. dom R ( [ u ] R = [ v ] R -> ( [ u ] R i^i [ v ] R ) =/= (/) ) <-> A. u e. dom R A. v e. dom R ( [ u ] R = [ v ] R -> ( [ u ] R i^i [ v ] R ) =/= (/) ) )
11	9 10	mpbi	|- A. u e. dom R A. v e. dom R ( [ u ] R = [ v ] R -> ( [ u ] R i^i [ v ] R ) =/= (/) )
12		dfdisjALTV5a	|- ( Disj R <-> ( A. u e. dom R A. v e. dom R ( ( [ u ] R i^i [ v ] R ) =/= (/) -> u = v ) /\ Rel R ) )
13	12	simplbi	|- ( Disj R -> A. u e. dom R A. v e. dom R ( ( [ u ] R i^i [ v ] R ) =/= (/) -> u = v ) )
14		r19.26-2	|- ( A. u e. dom R A. v e. dom R ( ( [ u ] R = [ v ] R -> ( [ u ] R i^i [ v ] R ) =/= (/) ) /\ ( ( [ u ] R i^i [ v ] R ) =/= (/) -> u = v ) ) <-> ( A. u e. dom R A. v e. dom R ( [ u ] R = [ v ] R -> ( [ u ] R i^i [ v ] R ) =/= (/) ) /\ A. u e. dom R A. v e. dom R ( ( [ u ] R i^i [ v ] R ) =/= (/) -> u = v ) ) )
15		pm3.33	|- ( ( ( [ u ] R = [ v ] R -> ( [ u ] R i^i [ v ] R ) =/= (/) ) /\ ( ( [ u ] R i^i [ v ] R ) =/= (/) -> u = v ) ) -> ( [ u ] R = [ v ] R -> u = v ) )
16	15	2ralimi	|- ( A. u e. dom R A. v e. dom R ( ( [ u ] R = [ v ] R -> ( [ u ] R i^i [ v ] R ) =/= (/) ) /\ ( ( [ u ] R i^i [ v ] R ) =/= (/) -> u = v ) ) -> A. u e. dom R A. v e. dom R ( [ u ] R = [ v ] R -> u = v ) )
17	14 16	sylbir	|- ( ( A. u e. dom R A. v e. dom R ( [ u ] R = [ v ] R -> ( [ u ] R i^i [ v ] R ) =/= (/) ) /\ A. u e. dom R A. v e. dom R ( ( [ u ] R i^i [ v ] R ) =/= (/) -> u = v ) ) -> A. u e. dom R A. v e. dom R ( [ u ] R = [ v ] R -> u = v ) )
18	11 13 17	sylancr	|- ( Disj R -> A. u e. dom R A. v e. dom R ( [ u ] R = [ v ] R -> u = v ) )