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	⊢ ( 𝑅 ∈ 𝑉 → ( Disj QMap 𝑅 ↔ ∀ 𝑢 ∃* 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		relqmap	⊢ Rel QMap 𝑅
2		dfdisjALTV	⊢ ( Disj QMap 𝑅 ↔ ( FunALTV ^◡ QMap 𝑅 ∧ Rel QMap 𝑅 ) )
3	1 2	mpbiran2	⊢ ( Disj QMap 𝑅 ↔ FunALTV ^◡ QMap 𝑅 )
4		funALTVfun	⊢ ( FunALTV ^◡ QMap 𝑅 ↔ Fun ^◡ QMap 𝑅 )
5	3 4	bitri	⊢ ( Disj QMap 𝑅 ↔ Fun ^◡ QMap 𝑅 )
6		nfv	⊢ Ⅎ 𝑡 𝑅 ∈ 𝑉
7		nfcv	⊢ Ⅎ 𝑡 dom 𝑅
8		nfcv	⊢ Ⅎ 𝑡 QMap 𝑅
9		df-qmap	⊢ QMap 𝑅 = ( 𝑡 ∈ dom 𝑅 ↦ [ 𝑡 ] 𝑅 )
10		resexg	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↾ dom 𝑅 ) ∈ V )
11		elecex	⊢ ( ( 𝑅 ↾ dom 𝑅 ) ∈ V → ( 𝑡 ∈ dom 𝑅 → [ 𝑡 ] 𝑅 ∈ V ) )
12	10 11	syl	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑡 ∈ dom 𝑅 → [ 𝑡 ] 𝑅 ∈ V ) )
13	12	imp	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑡 ∈ dom 𝑅 ) → [ 𝑡 ] 𝑅 ∈ V )
14	6 7 8 9 13	funcnvmpt	⊢ ( 𝑅 ∈ 𝑉 → ( Fun ^◡ QMap 𝑅 ↔ ∀ 𝑢 ∃* 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ) )
15	5 14	bitrid	⊢ ( 𝑅 ∈ 𝑉 → ( Disj QMap 𝑅 ↔ ∀ 𝑢 ∃* 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ) )