Metamath Proof Explorer

Definition df-part

Description: Define the partition predicate (read: A is a partition by R ). Alternative definition is dfpart2 . The binary partition and the partition predicate are the same if A and R are sets, cf. brpartspart . (Contributed by Peter Mazsa, 12-Aug-2021)

		Ref	Expression
	Assertion	df-part	\|- ( R Part A <-> ( Disj R /\ R DomainQs A ) )

Detailed syntax breakdown


 |-  R
 |-  A
 |-  R Part A
 |-  Disj R
 |-  R DomainQs A
 |-  ( Disj R /\ R DomainQs A )
 |-  ( R Part A <-> ( Disj R /\ R DomainQs A ) )

Step	Hyp	Ref	Expression
0		cR	\|- R
1		cA	\|- A
2	1 0	wpart	\|- R Part A
3	0	wdisjALTV	\|- Disj R
4	1 0	wdmqs	\|- R DomainQs A
5	3 4	wa	\|- ( Disj R /\ R DomainQs A )
6	2 5	wb	\|- ( R Part A <-> ( Disj R /\ R DomainQs A ) )