qmapeldisjsim

Description: Injectivity of coset map from QMap being disjoint (implication form): under the Disjs condition on QMap R , the coset assignment is injective on dom R . (Contributed by Peter Mazsa, 16-Feb-2026)

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

Proof

Step	Hyp	Ref	Expression
1		qmapeldisjs	Could not format ( R e. V -> ( QMap R e. Disjs <-> Disj QMap R ) ) : No typesetting found for \|- ( R e. V -> ( QMap R e. Disjs <-> Disj QMap R ) ) with typecode \|-
2		disjimeceqim2	Could not format ( Disj QMap R -> ( ( A e. dom QMap R /\ B e. dom QMap R ) -> ( [ A ] QMap R = [ B ] QMap R -> A = B ) ) ) : No typesetting found for \|- ( Disj QMap R -> ( ( A e. dom QMap R /\ B e. dom QMap R ) -> ( [ A ] QMap R = [ B ] QMap R -> A = B ) ) ) with typecode \|-
3		dmqmap	Could not format ( R e. V -> dom QMap R = dom R ) : No typesetting found for \|- ( R e. V -> dom QMap R = dom R ) with typecode \|-
4	3	eleq2d	Could not format ( R e. V -> ( A e. dom QMap R <-> A e. dom R ) ) : No typesetting found for \|- ( R e. V -> ( A e. dom QMap R <-> A e. dom R ) ) with typecode \|-
5	3	eleq2d	Could not format ( R e. V -> ( B e. dom QMap R <-> B e. dom R ) ) : No typesetting found for \|- ( R e. V -> ( B e. dom QMap R <-> B e. dom R ) ) with typecode \|-
6	4 5	anbi12d	Could not format ( R e. V -> ( ( A e. dom QMap R /\ B e. dom QMap R ) <-> ( A e. dom R /\ B e. dom R ) ) ) : No typesetting found for \|- ( R e. V -> ( ( A e. dom QMap R /\ B e. dom QMap R ) <-> ( A e. dom R /\ B e. dom R ) ) ) with typecode \|-
7	6	pm5.32i	Could not format ( ( R e. V /\ ( A e. dom QMap R /\ B e. dom QMap R ) ) <-> ( R e. V /\ ( A e. dom R /\ B e. dom R ) ) ) : No typesetting found for \|- ( ( R e. V /\ ( A e. dom QMap R /\ B e. dom QMap R ) ) <-> ( R e. V /\ ( A e. dom R /\ B e. dom R ) ) ) with typecode \|-
8	7	imbi1i	Could not format ( ( ( R e. V /\ ( A e. dom QMap R /\ B e. dom QMap R ) ) -> ( [ A ] QMap R = [ B ] QMap R -> A = B ) ) <-> ( ( R e. V /\ ( A e. dom R /\ B e. dom R ) ) -> ( [ A ] QMap R = [ B ] QMap R -> A = B ) ) ) : No typesetting found for \|- ( ( ( R e. V /\ ( A e. dom QMap R /\ B e. dom QMap R ) ) -> ( [ A ] QMap R = [ B ] QMap R -> A = B ) ) <-> ( ( R e. V /\ ( A e. dom R /\ B e. dom R ) ) -> ( [ A ] QMap R = [ B ] QMap R -> A = B ) ) ) with typecode \|-
9		ecqmap	Could not format ( A e. dom R -> [ A ] QMap R = { [ A ] R } ) : No typesetting found for \|- ( A e. dom R -> [ A ] QMap R = { [ A ] R } ) with typecode \|-
10		ecqmap	Could not format ( B e. dom R -> [ B ] QMap R = { [ B ] R } ) : No typesetting found for \|- ( B e. dom R -> [ B ] QMap R = { [ B ] R } ) with typecode \|-
11	9 10	eqeqan12d	Could not format ( ( A e. dom R /\ B e. dom R ) -> ( [ A ] QMap R = [ B ] QMap R <-> { [ A ] R } = { [ B ] R } ) ) : No typesetting found for \|- ( ( A e. dom R /\ B e. dom R ) -> ( [ A ] QMap R = [ B ] QMap R <-> { [ A ] R } = { [ B ] R } ) ) with typecode \|-
12	11	imbi1d	Could not format ( ( A e. dom R /\ B e. dom R ) -> ( ( [ A ] QMap R = [ B ] QMap R -> A = B ) <-> ( { [ A ] R } = { [ B ] R } -> A = B ) ) ) : No typesetting found for \|- ( ( A e. dom R /\ B e. dom R ) -> ( ( [ A ] QMap R = [ B ] QMap R -> A = B ) <-> ( { [ A ] R } = { [ B ] R } -> A = B ) ) ) with typecode \|-
13		ecexg	$⊢ R \in V \to [A] R \in V$
14		sneqbg	$⊢ [A] R \in V \to (\{[A] R\} = \{[B] R\} \leftrightarrow [A] R = [B] R)$
15	13 14	syl	$⊢ R \in V \to (\{[A] R\} = \{[B] R\} \leftrightarrow [A] R = [B] R)$
16	15	imbi1d	$⊢ R \in V \to ((\{[A] R\} = \{[B] R\} \to A = B) \leftrightarrow ([A] R = [B] R \to A = B))$
17	12 16	sylan9bbr	Could not format ( ( R e. V /\ ( A e. dom R /\ B e. dom R ) ) -> ( ( [ A ] QMap R = [ B ] QMap R -> A = B ) <-> ( [ A ] R = [ B ] R -> A = B ) ) ) : No typesetting found for \|- ( ( R e. V /\ ( A e. dom R /\ B e. dom R ) ) -> ( ( [ A ] QMap R = [ B ] QMap R -> A = B ) <-> ( [ A ] R = [ B ] R -> A = B ) ) ) with typecode \|-
18	17	pm5.74i	Could not format ( ( ( R e. V /\ ( A e. dom R /\ B e. dom R ) ) -> ( [ A ] QMap R = [ B ] QMap R -> A = B ) ) <-> ( ( R e. V /\ ( A e. dom R /\ B e. dom R ) ) -> ( [ A ] R = [ B ] R -> A = B ) ) ) : No typesetting found for \|- ( ( ( R e. V /\ ( A e. dom R /\ B e. dom R ) ) -> ( [ A ] QMap R = [ B ] QMap R -> A = B ) ) <-> ( ( R e. V /\ ( A e. dom R /\ B e. dom R ) ) -> ( [ A ] R = [ B ] R -> A = B ) ) ) with typecode \|-
19	8 18	bitri	Could not format ( ( ( R e. V /\ ( A e. dom QMap R /\ B e. dom QMap R ) ) -> ( [ A ] QMap R = [ B ] QMap R -> A = B ) ) <-> ( ( R e. V /\ ( A e. dom R /\ B e. dom R ) ) -> ( [ A ] R = [ B ] R -> A = B ) ) ) : No typesetting found for \|- ( ( ( R e. V /\ ( A e. dom QMap R /\ B e. dom QMap R ) ) -> ( [ A ] QMap R = [ B ] QMap R -> A = B ) ) <-> ( ( R e. V /\ ( A e. dom R /\ B e. dom R ) ) -> ( [ A ] R = [ B ] R -> A = B ) ) ) with typecode \|-
20		impexp	Could not format ( ( ( R e. V /\ ( A e. dom QMap R /\ B e. dom QMap R ) ) -> ( [ A ] QMap R = [ B ] QMap R -> A = B ) ) <-> ( R e. V -> ( ( A e. dom QMap R /\ B e. dom QMap R ) -> ( [ A ] QMap R = [ B ] QMap R -> A = B ) ) ) ) : No typesetting found for \|- ( ( ( R e. V /\ ( A e. dom QMap R /\ B e. dom QMap R ) ) -> ( [ A ] QMap R = [ B ] QMap R -> A = B ) ) <-> ( R e. V -> ( ( A e. dom QMap R /\ B e. dom QMap R ) -> ( [ A ] QMap R = [ B ] QMap R -> A = B ) ) ) ) with typecode \|-
21		impexp	$⊢ ((R \in V \land (A \in dom R \land B \in dom R)) \to ([A] R = [B] R \to A = B)) \leftrightarrow (R \in V \to ((A \in dom R \land B \in dom R) \to ([A] R = [B] R \to A = B)))$
22	19 20 21	3bitr3i	Could not format ( ( R e. V -> ( ( A e. dom QMap R /\ B e. dom QMap R ) -> ( [ A ] QMap R = [ B ] QMap R -> A = B ) ) ) <-> ( R e. V -> ( ( A e. dom R /\ B e. dom R ) -> ( [ A ] R = [ B ] R -> A = B ) ) ) ) : No typesetting found for \|- ( ( R e. V -> ( ( A e. dom QMap R /\ B e. dom QMap R ) -> ( [ A ] QMap R = [ B ] QMap R -> A = B ) ) ) <-> ( R e. V -> ( ( A e. dom R /\ B e. dom R ) -> ( [ A ] R = [ B ] R -> A = B ) ) ) ) with typecode \|-
23	22	pm5.74ri	Could not format ( R e. V -> ( ( ( A e. dom QMap R /\ B e. dom QMap R ) -> ( [ A ] QMap R = [ B ] QMap R -> A = B ) ) <-> ( ( A e. dom R /\ B e. dom R ) -> ( [ A ] R = [ B ] R -> A = B ) ) ) ) : No typesetting found for \|- ( R e. V -> ( ( ( A e. dom QMap R /\ B e. dom QMap R ) -> ( [ A ] QMap R = [ B ] QMap R -> A = B ) ) <-> ( ( A e. dom R /\ B e. dom R ) -> ( [ A ] R = [ B ] R -> A = B ) ) ) ) with typecode \|-
24	2 23	imbitrid	Could not format ( R e. V -> ( Disj QMap R -> ( ( A e. dom R /\ B e. dom R ) -> ( [ A ] R = [ B ] R -> A = B ) ) ) ) : No typesetting found for \|- ( R e. V -> ( Disj QMap R -> ( ( A e. dom R /\ B e. dom R ) -> ( [ A ] R = [ B ] R -> A = B ) ) ) ) with typecode \|-
25	1 24	sylbid	Could not format ( R e. V -> ( QMap R e. Disjs -> ( ( A e. dom R /\ B e. dom R ) -> ( [ A ] R = [ B ] R -> A = B ) ) ) ) : No typesetting found for \|- ( R e. V -> ( QMap R e. Disjs -> ( ( A e. dom R /\ B e. dom R ) -> ( [ A ] R = [ B ] R -> A = B ) ) ) ) with typecode \|-
26	25	3imp	Could not format ( ( R e. V /\ QMap R e. Disjs /\ ( A e. dom R /\ B e. dom R ) ) -> ( [ A ] R = [ B ] R -> A = B ) ) : No typesetting found for \|- ( ( R e. V /\ QMap R e. Disjs /\ ( A e. dom R /\ B e. dom R ) ) -> ( [ A ] R = [ B ] R -> A = B ) ) with typecode \|-

Metamath Proof Explorer

Theorem qmapeldisjsim

Proof