rnqmapeleldisjsim

Description: Element-disjointness of the quotient carrier forces coset disjointness. Supplies the "cosets don't overlap unless equal" direction, but expressed via ran QMap R (the quotient carrier) and ElDisjs . This is the structural reason Disjs needs a "carrier disjointness" level distinct from the "unique representatives" level. (Contributed by Peter Mazsa, 16-Feb-2026)

		Ref	Expression
	Assertion	rnqmapeleldisjsim	Could not format assertion : No typesetting found for \|- ( ( R e. V /\ ran QMap R e. ElDisjs /\ ( A e. dom R /\ B e. dom R ) ) -> ( ( [ A ] R i^i [ B ] R ) =/= (/) -> [ A ] R = [ B ] R ) ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		rnqmap	Could not format ran QMap R = ( dom R /. R ) : No typesetting found for \|- ran QMap R = ( dom R /. R ) with typecode \|-
2	1	eleq1i	Could not format ( ran QMap R e. ElDisjs <-> ( dom R /. R ) e. ElDisjs ) : No typesetting found for \|- ( ran QMap R e. ElDisjs <-> ( dom R /. R ) e. ElDisjs ) with typecode \|-
3		dmqsex	$⊢ R \in V \to dom R / R \in V$
4		eleldisjseldisj	$⊢ dom R / R \in V \to (dom R / R \in ElDisjs \leftrightarrow ElDisj (dom R / R))$
5	3 4	syl	$⊢ R \in V \to (dom R / R \in ElDisjs \leftrightarrow ElDisj (dom R / R))$
6	2 5	bitrid	Could not format ( R e. V -> ( ran QMap R e. ElDisjs <-> ElDisj ( dom R /. R ) ) ) : No typesetting found for \|- ( R e. V -> ( ran QMap R e. ElDisjs <-> ElDisj ( dom R /. R ) ) ) with typecode \|-
7		eldisjim3	$⊢ ElDisj (dom R / R) \to (([A] R \in (dom R / R) \land [B] R \in (dom R / R)) \to ([A] R \cap [B] R \neq \emptyset \to [A] R = [B] R))$
8		eceldmqs	$⊢ R \in V \to ([A] R \in (dom R / R) \leftrightarrow A \in dom R)$
9		eceldmqs	$⊢ R \in V \to ([B] R \in (dom R / R) \leftrightarrow B \in dom R)$
10	8 9	anbi12d	$⊢ R \in V \to (([A] R \in (dom R / R) \land [B] R \in (dom R / R)) \leftrightarrow (A \in dom R \land B \in dom R))$
11	10	imbi1d	$⊢ R \in V \to ((([A] R \in (dom R / R) \land [B] R \in (dom R / R)) \to ([A] R \cap [B] R \neq \emptyset \to [A] R = [B] R)) \leftrightarrow ((A \in dom R \land B \in dom R) \to ([A] R \cap [B] R \neq \emptyset \to [A] R = [B] R)))$
12	7 11	imbitrid	$⊢ R \in V \to (ElDisj (dom R / R) \to ((A \in dom R \land B \in dom R) \to ([A] R \cap [B] R \neq \emptyset \to [A] R = [B] R)))$
13	6 12	sylbid	Could not format ( R e. V -> ( ran QMap R e. ElDisjs -> ( ( A e. dom R /\ B e. dom R ) -> ( ( [ A ] R i^i [ B ] R ) =/= (/) -> [ A ] R = [ B ] R ) ) ) ) : No typesetting found for \|- ( R e. V -> ( ran QMap R e. ElDisjs -> ( ( A e. dom R /\ B e. dom R ) -> ( ( [ A ] R i^i [ B ] R ) =/= (/) -> [ A ] R = [ B ] R ) ) ) ) with typecode \|-
14	13	3imp	Could not format ( ( R e. V /\ ran QMap R e. ElDisjs /\ ( A e. dom R /\ B e. dom R ) ) -> ( ( [ A ] R i^i [ B ] R ) =/= (/) -> [ A ] R = [ B ] R ) ) : No typesetting found for \|- ( ( R e. V /\ ran QMap R e. ElDisjs /\ ( A e. dom R /\ B e. dom R ) ) -> ( ( [ A ] R i^i [ B ] R ) =/= (/) -> [ A ] R = [ B ] R ) ) with typecode \|-

Metamath Proof Explorer

Theorem rnqmapeleldisjsim

Proof