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 = { 𝑟 ∈ Rels ∣ ( ∀ 𝑥 ∃* 𝑢 ∈ ( dom 𝑟 / 𝑟 ) 𝑥 ∈ 𝑢 ∧ ∀ 𝑢 ∈ ( dom 𝑟 / 𝑟 ) ∃! 𝑡 ∈ dom 𝑟 𝑢 = [ 𝑡 ] 𝑟 ) }

Proof

Step	Hyp	Ref	Expression
1		eldisjs7	⊢ ( 𝑟 ∈ Disjs ↔ ( 𝑟 ∈ Rels ∧ ( ∀ 𝑥 ∃* 𝑢 ∈ ( dom 𝑟 / 𝑟 ) 𝑥 ∈ 𝑢 ∧ ∀ 𝑢 ∈ ( dom 𝑟 / 𝑟 ) ∃! 𝑡 ∈ dom 𝑟 𝑢 = [ 𝑡 ] 𝑟 ) ) )
2	1	eqrabi	⊢ Disjs = { 𝑟 ∈ Rels ∣ ( ∀ 𝑥 ∃* 𝑢 ∈ ( dom 𝑟 / 𝑟 ) 𝑥 ∈ 𝑢 ∧ ∀ 𝑢 ∈ ( dom 𝑟 / 𝑟 ) ∃! 𝑡 ∈ dom 𝑟 𝑢 = [ 𝑡 ] 𝑟 ) }