Theorem eldisjsim5

Description: Disjs is closed under QMap . If a relation is "disjoint-structured" ( Disjs ), then its canonical block map is also "disjoint-structured". This is the second "structure level" in Disjs : it expresses that the property is stable under passing to the canonical block map, a theme that mirrors Pet-grade stability at a different axis. (Contributed by Peter Mazsa, 15-Feb-2026)

	Ref	Expression
Assertion	eldisjsim5	⊢ ( 𝑅 ∈ Disjs → QMap 𝑅 ∈ Disjs )

Proof

Step	Hyp	Ref	Expression
1		eldisjsim1	⊢ ( 𝑅 ∈ Disjs → Disj 𝑅 )
2		disjimrmoeqec	⊢ ( Disj 𝑅 → ∃* 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 )
3	1 2	syl	⊢ ( 𝑅 ∈ Disjs → ∃* 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 )
4	3	alrimiv	⊢ ( 𝑅 ∈ Disjs → ∀ 𝑢 ∃* 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 )
5		disjqmap2	⊢ ( 𝑅 ∈ Disjs → ( Disj QMap 𝑅 ↔ ∀ 𝑢 ∃* 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ) )
6	4 5	mpbird	⊢ ( 𝑅 ∈ Disjs → Disj QMap 𝑅 )
7		qmapeldisjs	⊢ ( 𝑅 ∈ Disjs → ( QMap 𝑅 ∈ Disjs ↔ Disj QMap 𝑅 ) )
8	6 7	mpbird	⊢ ( 𝑅 ∈ Disjs → QMap 𝑅 ∈ Disjs )