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 R /. R ) /\ R e. Rels ) -> ( ( u e. dom R /\ v e. dom R ) -> ( ( [ u ] R i^i [ v ] R ) =/= (/) -> [ u ] R = [ v ] R ) ) )

Proof

Step	Hyp	Ref	Expression
1		eldisjim3	\|- ( ElDisj ( dom R /. R ) -> ( ( [ u ] R e. ( dom R /. R ) /\ [ v ] R e. ( dom R /. R ) ) -> ( ( [ u ] R i^i [ v ] R ) =/= (/) -> [ u ] R = [ v ] R ) ) )
2		eceldmqs	\|- ( R e. Rels -> ( [ u ] R e. ( dom R /. R ) <-> u e. dom R ) )
3		eceldmqs	\|- ( R e. Rels -> ( [ v ] R e. ( dom R /. R ) <-> v e. dom R ) )
4	2 3	anbi12d	\|- ( R e. Rels -> ( ( [ u ] R e. ( dom R /. R ) /\ [ v ] R e. ( dom R /. R ) ) <-> ( u e. dom R /\ v e. dom R ) ) )
5	4	imbi1d	\|- ( R e. Rels -> ( ( ( [ u ] R e. ( dom R /. R ) /\ [ v ] R e. ( dom R /. R ) ) -> ( ( [ u ] R i^i [ v ] R ) =/= (/) -> [ u ] R = [ v ] R ) ) <-> ( ( u e. dom R /\ v e. dom R ) -> ( ( [ u ] R i^i [ v ] R ) =/= (/) -> [ u ] R = [ v ] R ) ) ) )
6	1 5	imbitrid	\|- ( R e. Rels -> ( ElDisj ( dom R /. R ) -> ( ( u e. dom R /\ v e. dom R ) -> ( ( [ u ] R i^i [ v ] R ) =/= (/) -> [ u ] R = [ v ] R ) ) ) )
7	6	impcom	\|- ( ( ElDisj ( dom R /. R ) /\ R e. Rels ) -> ( ( u e. dom R /\ v e. dom R ) -> ( ( [ u ] R i^i [ v ] R ) =/= (/) -> [ u ] R = [ v ] R ) ) )