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	|- ( R e. V -> ( Disj QMap R <-> A. u E* t e. dom R u = [ t ] R ) )

Proof

Step	Hyp	Ref	Expression
1		relqmap	|- Rel QMap R
2		dfdisjALTV	|- ( Disj QMap R <-> ( FunALTV `' QMap R /\ Rel QMap R ) )
3	1 2	mpbiran2	|- ( Disj QMap R <-> FunALTV `' QMap R )
4		funALTVfun	|- ( FunALTV `' QMap R <-> Fun `' QMap R )
5	3 4	bitri	|- ( Disj QMap R <-> Fun `' QMap R )
6		nfv	|- F/ t R e. V
7		nfcv	|- F/_ t dom R
8		nfcv	|- F/_ t QMap R
9		df-qmap	|- QMap R = ( t e. dom R |-> [ t ] R )
10		resexg	|- ( R e. V -> ( R |` dom R ) e. _V )
11		elecex	|- ( ( R |` dom R ) e. _V -> ( t e. dom R -> [ t ] R e. _V ) )
12	10 11	syl	|- ( R e. V -> ( t e. dom R -> [ t ] R e. _V ) )
13	12	imp	|- ( ( R e. V /\ t e. dom R ) -> [ t ] R e. _V )
14	6 7 8 9 13	funcnvmpt	|- ( R e. V -> ( Fun `' QMap R <-> A. u E* t e. dom R u = [ t ] R ) )
15	5 14	bitrid	|- ( R e. V -> ( Disj QMap R <-> A. u E* t e. dom R u = [ t ] R ) )