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 R -> ElDisj ( dom R /. R ) )

Proof

Step	Hyp	Ref	Expression
1		disjim	|- ( Disj R -> EqvRel ,~ R )
2		disjdmqs	|- ( Disj R -> ( dom R /. R ) = ( dom ,~ R /. ,~ R ) )
3	2	eqcomd	|- ( Disj R -> ( dom ,~ R /. ,~ R ) = ( dom R /. R ) )
4		eqvrelqseqdisj2	|- ( ( EqvRel ,~ R /\ ( dom ,~ R /. ,~ R ) = ( dom R /. R ) ) -> ElDisj ( dom R /. R ) )
5	1 3 4	syl2anc	|- ( Disj R -> ElDisj ( dom R /. R ) )