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	|- ( R e. Disjs -> QMap R e. Disjs )

Proof

Step	Hyp	Ref	Expression
1		eldisjsim1	|- ( R e. Disjs -> Disj R )
2		disjimrmoeqec	|- ( Disj R -> E* t e. dom R u = [ t ] R )
3	1 2	syl	|- ( R e. Disjs -> E* t e. dom R u = [ t ] R )
4	3	alrimiv	|- ( R e. Disjs -> A. u E* t e. dom R u = [ t ] R )
5		disjqmap2	|- ( R e. Disjs -> ( Disj QMap R <-> A. u E* t e. dom R u = [ t ] R ) )
6	4 5	mpbird	|- ( R e. Disjs -> Disj QMap R )
7		qmapeldisjs	|- ( R e. Disjs -> ( QMap R e. Disjs <-> Disj QMap R ) )
8	6 7	mpbird	|- ( R e. Disjs -> QMap R e. Disjs )