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 𝑅 → ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → 𝑢 = 𝑣 ) )

Proof

Step	Hyp	Ref	Expression
1		ecdmn0	⊢ ( 𝑢 ∈ dom 𝑅 ↔ [ 𝑢 ] 𝑅 ≠ ∅ )
2	1	biimpi	⊢ ( 𝑢 ∈ dom 𝑅 → [ 𝑢 ] 𝑅 ≠ ∅ )
3		ineq2	⊢ ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → ( [ 𝑢 ] 𝑅 ∩ [ 𝑢 ] 𝑅 ) = ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) )
4		inidm	⊢ ( [ 𝑢 ] 𝑅 ∩ [ 𝑢 ] 𝑅 ) = [ 𝑢 ] 𝑅
5	3 4	eqtr3di	⊢ ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) = [ 𝑢 ] 𝑅 )
6	5	neeq1d	⊢ ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → ( ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ ↔ [ 𝑢 ] 𝑅 ≠ ∅ ) )
7	2 6	syl5ibrcom	⊢ ( 𝑢 ∈ dom 𝑅 → ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ ) )
8	7	rgen	⊢ ∀ 𝑢 ∈ dom 𝑅 ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ )
9	8	rgenw	⊢ ∀ 𝑣 ∈ dom 𝑅 ∀ 𝑢 ∈ dom 𝑅 ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ )
10		ralcom	⊢ ( ∀ 𝑣 ∈ dom 𝑅 ∀ 𝑢 ∈ dom 𝑅 ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ ) ↔ ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ ) )
11	9 10	mpbi	⊢ ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ )
12		dfdisjALTV5a	⊢ ( Disj 𝑅 ↔ ( ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ → 𝑢 = 𝑣 ) ∧ Rel 𝑅 ) )
13	12	simplbi	⊢ ( Disj 𝑅 → ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ → 𝑢 = 𝑣 ) )
14		r19.26-2	⊢ ( ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ ) ∧ ( ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ → 𝑢 = 𝑣 ) ) ↔ ( ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ ) ∧ ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ → 𝑢 = 𝑣 ) ) )
15		pm3.33	⊢ ( ( ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ ) ∧ ( ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ → 𝑢 = 𝑣 ) ) → ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → 𝑢 = 𝑣 ) )
16	15	2ralimi	⊢ ( ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ ) ∧ ( ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ → 𝑢 = 𝑣 ) ) → ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → 𝑢 = 𝑣 ) )
17	14 16	sylbir	⊢ ( ( ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ ) ∧ ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ → 𝑢 = 𝑣 ) ) → ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → 𝑢 = 𝑣 ) )
18	11 13 17	sylancr	⊢ ( Disj 𝑅 → ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → 𝑢 = 𝑣 ) )