This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) }