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

Metamath Proof Explorer

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