Metamath Proof Explorer

Theorem eldisjdmqsim

Description: Shared output implies equal cosets (under ElDisj of quotient): if u and v both relate to the same x , then their cosets intersect, hence must coincide under quotient ElDisj . (Contributed by Peter Mazsa, 10-Feb-2026)

Ref Expression
Assertion eldisjdmqsim 
|- ( ( ElDisj ( dom R /. R ) /\ R e. Rels ) -> ( ( u R x /\ v R x ) -> [ u ] R = [ v ] R ) )

Proof

Step Hyp Ref Expression
1 elin 
 |-  ( x e. ( [ u ] R i^i [ v ] R ) <-> ( x e. [ u ] R /\ x e. [ v ] R ) )
2 elecALTV 
 |-  ( ( u e. _V /\ x e. _V ) -> ( x e. [ u ] R <-> u R x ) )
3 2 el2v 
 |-  ( x e. [ u ] R <-> u R x )
4 elecALTV 
 |-  ( ( v e. _V /\ x e. _V ) -> ( x e. [ v ] R <-> v R x ) )
5 4 el2v 
 |-  ( x e. [ v ] R <-> v R x )
6 3 5 anbi12i 
 |-  ( ( x e. [ u ] R /\ x e. [ v ] R ) <-> ( u R x /\ v R x ) )
7 1 6 bitr2i 
 |-  ( ( u R x /\ v R x ) <-> x e. ( [ u ] R i^i [ v ] R ) )
8 ne0i 
 |-  ( x e. ( [ u ] R i^i [ v ] R ) -> ( [ u ] R i^i [ v ] R ) =/= (/) )
9 7 8 sylbi 
 |-  ( ( u R x /\ v R x ) -> ( [ u ] R i^i [ v ] R ) =/= (/) )
10 19.8a 
 |-  ( u R x -> E. x u R x )
11 eldmg 
 |-  ( u e. _V -> ( u e. dom R <-> E. x u R x ) )
12 11 elv 
 |-  ( u e. dom R <-> E. x u R x )
13 10 12 sylibr 
 |-  ( u R x -> u e. dom R )
14 19.8a 
 |-  ( v R x -> E. x v R x )
15 eldmg 
 |-  ( v e. _V -> ( v e. dom R <-> E. x v R x ) )
16 15 elv 
 |-  ( v e. dom R <-> E. x v R x )
17 14 16 sylibr 
 |-  ( v R x -> v e. dom R )
18 13 17 anim12i 
 |-  ( ( u R x /\ v R x ) -> ( u e. dom R /\ v e. dom R ) )
19 eceldmqs 
 |-  ( R e. Rels -> ( [ u ] R e. ( dom R /. R ) <-> u e. dom R ) )
20 eceldmqs 
 |-  ( R e. Rels -> ( [ v ] R e. ( dom R /. R ) <-> v e. dom R ) )
21 19 20 anbi12d 
 |-  ( R e. Rels -> ( ( [ u ] R e. ( dom R /. R ) /\ [ v ] R e. ( dom R /. R ) ) <-> ( u e. dom R /\ v e. dom R ) ) )
22 18 21 imbitrrid 
 |-  ( R e. Rels -> ( ( u R x /\ v R x ) -> ( [ u ] R e. ( dom R /. R ) /\ [ v ] R e. ( dom R /. R ) ) ) )
23 22 adantl 
 |-  ( ( ElDisj ( dom R /. R ) /\ R e. Rels ) -> ( ( u R x /\ v R x ) -> ( [ u ] R e. ( dom R /. R ) /\ [ v ] R e. ( dom R /. R ) ) ) )
24 eldisjim3 
 |-  ( ElDisj ( dom R /. R ) -> ( ( [ u ] R e. ( dom R /. R ) /\ [ v ] R e. ( dom R /. R ) ) -> ( ( [ u ] R i^i [ v ] R ) =/= (/) -> [ u ] R = [ v ] R ) ) )
25 24 adantr 
 |-  ( ( ElDisj ( dom R /. R ) /\ R e. Rels ) -> ( ( [ u ] R e. ( dom R /. R ) /\ [ v ] R e. ( dom R /. R ) ) -> ( ( [ u ] R i^i [ v ] R ) =/= (/) -> [ u ] R = [ v ] R ) ) )
26 23 25 syld 
 |-  ( ( ElDisj ( dom R /. R ) /\ R e. Rels ) -> ( ( u R x /\ v R x ) -> ( ( [ u ] R i^i [ v ] R ) =/= (/) -> [ u ] R = [ v ] R ) ) )
27 9 26 mpdi 
 |-  ( ( ElDisj ( dom R /. R ) /\ R e. Rels ) -> ( ( u R x /\ v R x ) -> [ u ] R = [ v ] R ) )