Definition df-parts

Description: Define the class of all partitions, cf. the comment of df-disjs . Partitions are disjoints on domain quotients (or: domain quotients restricted to disjoints).

This is a more general meaning of partition than we we are familiar with: the conventional meaning of partition (e.g. partition A of X , Halmos p. 28: "A partition of X is a disjoint collection A of non-empty subsets of X whose union is X ", or Definition 35, Suppes p. 83., cf. https://oeis.org/A000110 ) is what we call membership partition here, cf. dfmembpart2 .

The binary partitions relation and the partition predicate are the same, that is, ( R Parts A <-> R Part A ) if A and R are sets, cf. brpartspart . (Contributed by Peter Mazsa, 26-Jun-2021)

	Ref	Expression
Assertion	df-parts	Could not format assertion : No typesetting found for |- Parts = ( DomainQss |` Disjs ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cparts	Could not format Parts : No typesetting found for class Parts with typecode class
1		cdmqss	$$class\mathrm{DomainQss}$$
2		cdisjs	$$class\mathrm{Disjs}$$
3	1 2	cres	$$class\left({\mathrm{DomainQss}\upharpoonright }_{\mathrm{Disjs}}\right)$$
4	0 3	wceq	Could not format Parts = ( DomainQss |` Disjs ) : No typesetting found for wff Parts = ( DomainQss |` Disjs ) with typecode wff