Theorem eldisjdmqsim2

Description: ElDisj of quotient implies coset-disjointness (domain form). Converts element-disjointness of the quotient carrier into a usable "cosets don't overlap unless equal" rule. (Contributed by Peter Mazsa, 10-Feb-2026)

	Ref	Expression
Assertion	eldisjdmqsim2	⊢ ( ( ElDisj ( dom 𝑅 / 𝑅 ) ∧ 𝑅 ∈ Rels ) → ( ( 𝑢 ∈ dom 𝑅 ∧ 𝑣 ∈ dom 𝑅 ) → ( ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ → [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eldisjim3	⊢ ( ElDisj ( dom 𝑅 / 𝑅 ) → ( ( [ 𝑢 ] 𝑅 ∈ ( dom 𝑅 / 𝑅 ) ∧ [ 𝑣 ] 𝑅 ∈ ( dom 𝑅 / 𝑅 ) ) → ( ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ → [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 ) ) )
2		eceldmqs	⊢ ( 𝑅 ∈ Rels → ( [ 𝑢 ] 𝑅 ∈ ( dom 𝑅 / 𝑅 ) ↔ 𝑢 ∈ dom 𝑅 ) )
3		eceldmqs	⊢ ( 𝑅 ∈ Rels → ( [ 𝑣 ] 𝑅 ∈ ( dom 𝑅 / 𝑅 ) ↔ 𝑣 ∈ dom 𝑅 ) )
4	2 3	anbi12d	⊢ ( 𝑅 ∈ Rels → ( ( [ 𝑢 ] 𝑅 ∈ ( dom 𝑅 / 𝑅 ) ∧ [ 𝑣 ] 𝑅 ∈ ( dom 𝑅 / 𝑅 ) ) ↔ ( 𝑢 ∈ dom 𝑅 ∧ 𝑣 ∈ dom 𝑅 ) ) )
5	4	imbi1d	⊢ ( 𝑅 ∈ Rels → ( ( ( [ 𝑢 ] 𝑅 ∈ ( dom 𝑅 / 𝑅 ) ∧ [ 𝑣 ] 𝑅 ∈ ( dom 𝑅 / 𝑅 ) ) → ( ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ → [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 ) ) ↔ ( ( 𝑢 ∈ dom 𝑅 ∧ 𝑣 ∈ dom 𝑅 ) → ( ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ → [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 ) ) ) )
6	1 5	imbitrid	⊢ ( 𝑅 ∈ Rels → ( ElDisj ( dom 𝑅 / 𝑅 ) → ( ( 𝑢 ∈ dom 𝑅 ∧ 𝑣 ∈ dom 𝑅 ) → ( ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ → [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 ) ) ) )
7	6	impcom	⊢ ( ( ElDisj ( dom 𝑅 / 𝑅 ) ∧ 𝑅 ∈ Rels ) → ( ( 𝑢 ∈ dom 𝑅 ∧ 𝑣 ∈ dom 𝑅 ) → ( ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ → [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 ) ) )