This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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