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 𝑅 𝑢 = [ 𝑡 ] 𝑅 ) )