This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ Ⅎ t R \in V$
7		nfcv	$⊢ \underline{Ⅎ} t 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 ↾}_{dom R} \in V$
11		elecex	$⊢ {R ↾}_{dom R} \in V \to (t \in dom R \to [t] R \in V)$
12	10 11	syl	$⊢ R \in V \to (t \in dom R \to [t] R \in V)$
13	12	imp	$⊢ (R \in V \land t \in dom R) \to [t] R \in 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 \|-