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	|- Parts = ( DomainQss |` Disjs )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cparts	|- Parts
1		cdmqss	|- DomainQss
2		cdisjs	|- Disjs
3	1 2	cres	|- ( DomainQss |` Disjs )
4	0 3	wceq	|- Parts = ( DomainQss |` Disjs )