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 ∈ Rels | ∀ x ∃* u ∈ dom ⁡ r / r x ∈ u ∧ ∀ u ∈ dom ⁡ r / r ∃! t ∈ dom ⁡ r u = t r

Proof

Step Hyp Ref Expression
1 eldisjs7 ⊢ r ∈ Disjs ↔ r ∈ Rels ∧ ∀ x ∃* u ∈ dom ⁡ r / r x ∈ u ∧ ∀ u ∈ dom ⁡ r / r ∃! t ∈ dom ⁡ r u = t r
2 1 eqrabi ⊢ Disjs = r ∈ Rels | ∀ x ∃* u ∈ dom ⁡ r / r x ∈ u ∧ ∀ u ∈ dom ⁡ r / r ∃! t ∈ dom ⁡ r u = t r