Theorem dfdisjs6

Description: Alternate definition of the class of disjoints (via quotient-map stability). Disjs is the class of relations r whose quotient-map QMap r is again disjoint and whose induced quotient-carrier is element-disjoint. This is the definitional "stability-by-decomposition" packaging of disjointness: it builds Disjs from two internal layers (i) a carrier-layer constraint and (ii) a map-layer closure constraint. This is deliberately different from "u R x" style definitions: it makes the carrier of blocks and the uniqueness-of-representatives discipline first-class and reusable (via QMap ) rather than implicit. (Contributed by Peter Mazsa, 16-Feb-2026)

	Ref	Expression
Assertion	dfdisjs6	Could not format assertion : No typesetting found for |- Disjs = { r e. Rels | ( ran QMap r e. ElDisjs /\ QMap r e. Disjs ) } with typecode |-

Proof

Step	Hyp	Ref	Expression
1		eldisjs6	Could not format ( r e. Disjs <-> ( r e. Rels /\ ( ran QMap r e. ElDisjs /\ QMap r e. Disjs ) ) ) : No typesetting found for |- ( r e. Disjs <-> ( r e. Rels /\ ( ran QMap r e. ElDisjs /\ QMap r e. Disjs ) ) ) with typecode |-
2	1	eqrabi	Could not format Disjs = { r e. Rels | ( ran QMap r e. ElDisjs /\ QMap r e. Disjs ) } : No typesetting found for |- Disjs = { r e. Rels | ( ran QMap r e. ElDisjs /\ QMap r e. Disjs ) } with typecode |-