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	⊢ Disjs = { 𝑟 ∈ Rels ∣ ( ran QMap 𝑟 ∈ ElDisjs ∧ QMap 𝑟 ∈ Disjs ) }

Proof

Step	Hyp	Ref	Expression
1		eldisjs6	⊢ ( 𝑟 ∈ Disjs ↔ ( 𝑟 ∈ Rels ∧ ( ran QMap 𝑟 ∈ ElDisjs ∧ QMap 𝑟 ∈ Disjs ) ) )
2	1	eqrabi	⊢ Disjs = { 𝑟 ∈ Rels ∣ ( ran QMap 𝑟 ∈ ElDisjs ∧ QMap 𝑟 ∈ Disjs ) }