Theorem dfdisjs7

Description: Alternate definition of the class of disjoints (via carrier disjointness + unique representatives). Ideology-free normal form of dfdisjs6 : "blocks cover their elements" ( E* ) and "each block has a unique generator" ( E! ), expressed entirely at the quotient-carrier level. Same class as dfdisjs6 , but presented in fully expanded E* / E! form over the quotient-carrier ( dom r /. r ) . Makes explicit (a) element-disjointness of the quotient-carrier and (b) unique representative existence for each block. These are exactly the two conditions that rule out type-confusions (blocks vs witnesses) and ensure canonical decomposition. This is the form that best supports analogy arguments with df-petparts and with successor-style uniqueness patterns. (Contributed by Peter Mazsa, 16-Feb-2026)

	Ref	Expression
Assertion	dfdisjs7	|- Disjs = { r e. Rels | ( A. x E* u e. ( dom r /. r ) x e. u /\ A. u e. ( dom r /. r ) E! t e. dom r u = [ t ] r ) }

Proof

Step	Hyp	Ref	Expression
1		eldisjs7	|- ( r e. Disjs <-> ( r e. Rels /\ ( A. x E* u e. ( dom r /. r ) x e. u /\ A. u e. ( dom r /. r ) E! t e. dom r u = [ t ] r ) ) )
2	1	eqrabi	|- Disjs = { r e. Rels | ( A. x E* u e. ( dom r /. r ) x e. u /\ A. u e. ( dom r /. r ) E! t e. dom r u = [ t ] r ) }