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 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 ) )