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 𝑅 / 𝑅 ) ∧ 𝑅 ∈ Rels ) → ( ( 𝑢 𝑅 𝑥 ∧ 𝑣 𝑅 𝑥 ) → [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 ) )

Proof

Step Hyp Ref Expression
1 elin ⊢ ( 𝑥 ∈ ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ↔ ( 𝑥 ∈ [ 𝑢 ] 𝑅 ∧ 𝑥 ∈ [ 𝑣 ] 𝑅 ) )
2 elecALTV ⊢ ( ( 𝑢 ∈ V ∧ 𝑥 ∈ V ) → ( 𝑥 ∈ [ 𝑢 ] 𝑅 ↔ 𝑢 𝑅 𝑥 ) )
3 2 el2v ⊢ ( 𝑥 ∈ [ 𝑢 ] 𝑅 ↔ 𝑢 𝑅 𝑥 )
4 elecALTV ⊢ ( ( 𝑣 ∈ V ∧ 𝑥 ∈ V ) → ( 𝑥 ∈ [ 𝑣 ] 𝑅 ↔ 𝑣 𝑅 𝑥 ) )
5 4 el2v ⊢ ( 𝑥 ∈ [ 𝑣 ] 𝑅 ↔ 𝑣 𝑅 𝑥 )
6 3 5 anbi12i ⊢ ( ( 𝑥 ∈ [ 𝑢 ] 𝑅 ∧ 𝑥 ∈ [ 𝑣 ] 𝑅 ) ↔ ( 𝑢 𝑅 𝑥 ∧ 𝑣 𝑅 𝑥 ) )
7 1 6 bitr2i ⊢ ( ( 𝑢 𝑅 𝑥 ∧ 𝑣 𝑅 𝑥 ) ↔ 𝑥 ∈ ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) )
8 ne0i ⊢ ( 𝑥 ∈ ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) → ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ )
9 7 8 sylbi ⊢ ( ( 𝑢 𝑅 𝑥 ∧ 𝑣 𝑅 𝑥 ) → ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ )
10 19.8a ⊢ ( 𝑢 𝑅 𝑥 → ∃ 𝑥 𝑢 𝑅 𝑥 )
11 eldmg ⊢ ( 𝑢 ∈ V → ( 𝑢 ∈ dom 𝑅 ↔ ∃ 𝑥 𝑢 𝑅 𝑥 ) )
12 11 elv ⊢ ( 𝑢 ∈ dom 𝑅 ↔ ∃ 𝑥 𝑢 𝑅 𝑥 )
13 10 12 sylibr ⊢ ( 𝑢 𝑅 𝑥 → 𝑢 ∈ dom 𝑅 )
14 19.8a ⊢ ( 𝑣 𝑅 𝑥 → ∃ 𝑥 𝑣 𝑅 𝑥 )
15 eldmg ⊢ ( 𝑣 ∈ V → ( 𝑣 ∈ dom 𝑅 ↔ ∃ 𝑥 𝑣 𝑅 𝑥 ) )
16 15 elv ⊢ ( 𝑣 ∈ dom 𝑅 ↔ ∃ 𝑥 𝑣 𝑅 𝑥 )
17 14 16 sylibr ⊢ ( 𝑣 𝑅 𝑥 → 𝑣 ∈ dom 𝑅 )
18 13 17 anim12i ⊢ ( ( 𝑢 𝑅 𝑥 ∧ 𝑣 𝑅 𝑥 ) → ( 𝑢 ∈ dom 𝑅 ∧ 𝑣 ∈ dom 𝑅 ) )
19 eceldmqs ⊢ ( 𝑅 ∈ Rels → ( [ 𝑢 ] 𝑅 ∈ ( dom 𝑅 / 𝑅 ) ↔ 𝑢 ∈ dom 𝑅 ) )
20 eceldmqs ⊢ ( 𝑅 ∈ Rels → ( [ 𝑣 ] 𝑅 ∈ ( dom 𝑅 / 𝑅 ) ↔ 𝑣 ∈ dom 𝑅 ) )
21 19 20 anbi12d ⊢ ( 𝑅 ∈ Rels → ( ( [ 𝑢 ] 𝑅 ∈ ( dom 𝑅 / 𝑅 ) ∧ [ 𝑣 ] 𝑅 ∈ ( dom 𝑅 / 𝑅 ) ) ↔ ( 𝑢 ∈ dom 𝑅 ∧ 𝑣 ∈ dom 𝑅 ) ) )
22 18 21 imbitrrid ⊢ ( 𝑅 ∈ Rels → ( ( 𝑢 𝑅 𝑥 ∧ 𝑣 𝑅 𝑥 ) → ( [ 𝑢 ] 𝑅 ∈ ( dom 𝑅 / 𝑅 ) ∧ [ 𝑣 ] 𝑅 ∈ ( dom 𝑅 / 𝑅 ) ) ) )
23 22 adantl ⊢ ( ( ElDisj ( dom 𝑅 / 𝑅 ) ∧ 𝑅 ∈ Rels ) → ( ( 𝑢 𝑅 𝑥 ∧ 𝑣 𝑅 𝑥 ) → ( [ 𝑢 ] 𝑅 ∈ ( dom 𝑅 / 𝑅 ) ∧ [ 𝑣 ] 𝑅 ∈ ( dom 𝑅 / 𝑅 ) ) ) )
24 eldisjim3 ⊢ ( ElDisj ( dom 𝑅 / 𝑅 ) → ( ( [ 𝑢 ] 𝑅 ∈ ( dom 𝑅 / 𝑅 ) ∧ [ 𝑣 ] 𝑅 ∈ ( dom 𝑅 / 𝑅 ) ) → ( ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ → [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 ) ) )
25 24 adantr ⊢ ( ( ElDisj ( dom 𝑅 / 𝑅 ) ∧ 𝑅 ∈ Rels ) → ( ( [ 𝑢 ] 𝑅 ∈ ( dom 𝑅 / 𝑅 ) ∧ [ 𝑣 ] 𝑅 ∈ ( dom 𝑅 / 𝑅 ) ) → ( ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ → [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 ) ) )
26 23 25 syld ⊢ ( ( ElDisj ( dom 𝑅 / 𝑅 ) ∧ 𝑅 ∈ Rels ) → ( ( 𝑢 𝑅 𝑥 ∧ 𝑣 𝑅 𝑥 ) → ( ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ → [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 ) ) )
27 9 26 mpdi ⊢ ( ( ElDisj ( dom 𝑅 / 𝑅 ) ∧ 𝑅 ∈ Rels ) → ( ( 𝑢 𝑅 𝑥 ∧ 𝑣 𝑅 𝑥 ) → [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 ) )