Theorem 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 \left[A\right]R\in \mathrm{V}$$
14		sneqbg	$$⊢\left[A\right]R\in \mathrm{V}\to \left(\left\{\left[A\right]R\right\}=\left\{\left[B\right]R\right\}\leftrightarrow \left[A\right]R=\left[B\right]R\right)$$
15	13 14	syl	$$⊢R\in V\to \left(\left\{\left[A\right]R\right\}=\left\{\left[B\right]R\right\}\leftrightarrow \left[A\right]R=\left[B\right]R\right)$$
16	15	imbi1d	$$⊢R\in V\to \left(\left(\left\{\left[A\right]R\right\}=\left\{\left[B\right]R\right\}\to A=B\right)\leftrightarrow \left(\left[A\right]R=\left[B\right]R\to A=B\right)\right)$$
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	$$⊢\left(\left(R\in V\wedge \left(A\in \mathrm{dom}R\wedge B\in \mathrm{dom}R\right)\right)\to \left(\left[A\right]R=\left[B\right]R\to A=B\right)\right)\leftrightarrow \left(R\in V\to \left(\left(A\in \mathrm{dom}R\wedge B\in \mathrm{dom}R\right)\to \left(\left[A\right]R=\left[B\right]R\to A=B\right)\right)\right)$$
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 |-