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	Could not format assertion : No typesetting found for |- ( R e. Disjs -> QMap R e. Disjs ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		eldisjsim1	$$⊢R\in \mathrm{Disjs}\to DisjR$$
2		disjimrmoeqec	$$⊢DisjR\to {\exists }^{*}t\in \mathrm{dom}Ru=\left[t\right]R$$
3	1 2	syl	$$⊢R\in \mathrm{Disjs}\to {\exists }^{*}t\in \mathrm{dom}Ru=\left[t\right]R$$
4	3	alrimiv	$$⊢R\in \mathrm{Disjs}\to \forall u{\exists }^{*}t\in \mathrm{dom}Ru=\left[t\right]R$$
5		disjqmap2	Could not format ( R e. Disjs -> ( Disj QMap R <-> A. u E* t e. dom R u = [ t ] R ) ) : No typesetting found for |- ( R e. Disjs -> ( Disj QMap R <-> A. u E* t e. dom R u = [ t ] R ) ) with typecode |-
6	4 5	mpbird	Could not format ( R e. Disjs -> Disj QMap R ) : No typesetting found for |- ( R e. Disjs -> Disj QMap R ) with typecode |-
7		qmapeldisjs	Could not format ( R e. Disjs -> ( QMap R e. Disjs <-> Disj QMap R ) ) : No typesetting found for |- ( R e. Disjs -> ( QMap R e. Disjs <-> Disj QMap R ) ) with typecode |-
8	6 7	mpbird	Could not format ( R e. Disjs -> QMap R e. Disjs ) : No typesetting found for |- ( R e. Disjs -> QMap R e. Disjs ) with typecode |-