Theorem disjqmap2

Description: Disjointness of QMap equals E* -generation. Pairs with disjqmap and raldmqseu to move between E* and E! depending on context. (Contributed by Peter Mazsa, 12-Feb-2026)

	Ref	Expression
Assertion	disjqmap2	Could not format assertion : No typesetting found for |- ( R e. V -> ( Disj QMap R <-> A. u E* t e. dom R u = [ t ] R ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		relqmap	Could not format Rel QMap R : No typesetting found for |- Rel QMap R with typecode |-
2		dfdisjALTV	Could not format ( Disj QMap R <-> ( FunALTV `' QMap R /\ Rel QMap R ) ) : No typesetting found for |- ( Disj QMap R <-> ( FunALTV `' QMap R /\ Rel QMap R ) ) with typecode |-
3	1 2	mpbiran2	Could not format ( Disj QMap R <-> FunALTV `' QMap R ) : No typesetting found for |- ( Disj QMap R <-> FunALTV `' QMap R ) with typecode |-
4		funALTVfun	Could not format ( FunALTV `' QMap R <-> Fun `' QMap R ) : No typesetting found for |- ( FunALTV `' QMap R <-> Fun `' QMap R ) with typecode |-
5	3 4	bitri	Could not format ( Disj QMap R <-> Fun `' QMap R ) : No typesetting found for |- ( Disj QMap R <-> Fun `' QMap R ) with typecode |-
6		nfv	$$⊢ℲtR\in V$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}t\mathrm{dom}R$$
8		nfcv	Could not format F/_ t QMap R : No typesetting found for |- F/_ t QMap R with typecode |-
9		df-qmap	Could not format QMap R = ( t e. dom R |-> [ t ] R ) : No typesetting found for |- QMap R = ( t e. dom R |-> [ t ] R ) with typecode |-
10		resexg	$$⊢R\in V\to {R\upharpoonright }_{\mathrm{dom}R}\in \mathrm{V}$$
11		elecex	$$⊢{R\upharpoonright }_{\mathrm{dom}R}\in \mathrm{V}\to \left(t\in \mathrm{dom}R\to \left[t\right]R\in \mathrm{V}\right)$$
12	10 11	syl	$$⊢R\in V\to \left(t\in \mathrm{dom}R\to \left[t\right]R\in \mathrm{V}\right)$$
13	12	imp	$$⊢\left(R\in V\wedge t\in \mathrm{dom}R\right)\to \left[t\right]R\in \mathrm{V}$$
14	6 7 8 9 13	funcnvmpt	Could not format ( R e. V -> ( Fun `' QMap R <-> A. u E* t e. dom R u = [ t ] R ) ) : No typesetting found for |- ( R e. V -> ( Fun `' QMap R <-> A. u E* t e. dom R u = [ t ] R ) ) with typecode |-
15	5 14	bitrid	Could not format ( R e. V -> ( Disj QMap R <-> A. u E* t e. dom R u = [ t ] R ) ) : No typesetting found for |- ( R e. V -> ( Disj QMap R <-> A. u E* t e. dom R u = [ t ] R ) ) with typecode |-