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 Disjs \to Disj R$
2		disjimrmoeqec	$⊢ Disj R \to \exists^{*} t \in dom R u = [t] R$
3	1 2	syl	$⊢ R \in Disjs \to \exists^{*} t \in dom R u = [t] R$
4	3	alrimiv	$⊢ R \in Disjs \to \forall u \exists^{*} t \in dom R u = [t] 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 \|-

Metamath Proof Explorer

Theorem eldisjsim5

Proof