Theorem disjimeldisjdmqs

Description: Disj implies element-disjoint quotient carrier. Supplies the carrier-disjointness half of the Disjs pattern: under Disj R , the coset family is element-disjoint. (Contributed by Peter Mazsa, 5-Feb-2026)

	Ref	Expression
Assertion	disjimeldisjdmqs	⊢ ( Disj 𝑅 → ElDisj ( dom 𝑅 / 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		disjim	⊢ ( Disj 𝑅 → EqvRel ≀ 𝑅 )
2		disjdmqs	⊢ ( Disj 𝑅 → ( dom 𝑅 / 𝑅 ) = ( dom ≀ 𝑅 / ≀ 𝑅 ) )
3	2	eqcomd	⊢ ( Disj 𝑅 → ( dom ≀ 𝑅 / ≀ 𝑅 ) = ( dom 𝑅 / 𝑅 ) )
4		eqvrelqseqdisj2	⊢ ( ( EqvRel ≀ 𝑅 ∧ ( dom ≀ 𝑅 / ≀ 𝑅 ) = ( dom 𝑅 / 𝑅 ) ) → ElDisj ( dom 𝑅 / 𝑅 ) )
5	1 3 4	syl2anc	⊢ ( Disj 𝑅 → ElDisj ( dom 𝑅 / 𝑅 ) )