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

Metamath Proof Explorer

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 \to ElDisj (dom R / R)$

Proof

Step	Hyp	Ref	Expression
1		disjim	$⊢ Disj R \to EqvRel ≀ R$
2		disjdmqs	$⊢ Disj R \to dom R / R = dom ≀ R / ≀ R$
3	2	eqcomd	$⊢ Disj R \to dom ≀ R / ≀ R = dom R / R$
4		eqvrelqseqdisj2	$⊢ (EqvRel ≀ R \land dom ≀ R / ≀ R = dom R / R) \to ElDisj (dom R / R)$
5	1 3 4	syl2anc	$⊢ Disj R \to ElDisj (dom R / R)$