Theorem brpartspart

Description: Binary partition and the partition predicate are the same if A and R are sets. (Contributed by Peter Mazsa, 5-Sep-2021)

	Ref	Expression
Assertion	brpartspart	Could not format assertion : No typesetting found for |- ( ( A e. V /\ R e. W ) -> ( R Parts A <-> R Part A ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		eldisjsdisj	$$⊢R\in W\to \left(R\in \mathrm{Disjs}\leftrightarrow DisjR\right)$$
2	1	adantl	$$⊢\left(A\in V\wedge R\in W\right)\to \left(R\in \mathrm{Disjs}\leftrightarrow DisjR\right)$$
3		brdmqssqs	$$⊢\left(A\in V\wedge R\in W\right)\to \left(R\mathrm{DomainQss}A\leftrightarrow RDomainQsA\right)$$
4	2 3	anbi12d	$$⊢\left(A\in V\wedge R\in W\right)\to \left(\left(R\in \mathrm{Disjs}\wedge R\mathrm{DomainQss}A\right)\leftrightarrow \left(DisjR\wedge RDomainQsA\right)\right)$$
5		brparts	Could not format ( A e. V -> ( R Parts A <-> ( R e. Disjs /\ R DomainQss A ) ) ) : No typesetting found for |- ( A e. V -> ( R Parts A <-> ( R e. Disjs /\ R DomainQss A ) ) ) with typecode |-
6	5	adantr	Could not format ( ( A e. V /\ R e. W ) -> ( R Parts A <-> ( R e. Disjs /\ R DomainQss A ) ) ) : No typesetting found for |- ( ( A e. V /\ R e. W ) -> ( R Parts A <-> ( R e. Disjs /\ R DomainQss A ) ) ) with typecode |-
7		df-part	Could not format ( R Part A <-> ( Disj R /\ R DomainQs A ) ) : No typesetting found for |- ( R Part A <-> ( Disj R /\ R DomainQs A ) ) with typecode |-
8	7	a1i	Could not format ( ( A e. V /\ R e. W ) -> ( R Part A <-> ( Disj R /\ R DomainQs A ) ) ) : No typesetting found for |- ( ( A e. V /\ R e. W ) -> ( R Part A <-> ( Disj R /\ R DomainQs A ) ) ) with typecode |-
9	4 6 8	3bitr4d	Could not format ( ( A e. V /\ R e. W ) -> ( R Parts A <-> R Part A ) ) : No typesetting found for |- ( ( A e. V /\ R e. W ) -> ( R Parts A <-> R Part A ) ) with typecode |-