Theorem brparts2

Description: Binary partitions relation. (Contributed by Peter Mazsa, 30-Dec-2021)

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

Proof

Step	Hyp	Ref	Expression
1		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 |-
2	1	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 |-
3		brdmqss	$$⊢\left(A\in V\wedge R\in W\right)\to \left(R\mathrm{DomainQss}A\leftrightarrow \mathrm{dom}R/R=A\right)$$
4	3	anbi2d	$$⊢\left(A\in V\wedge R\in W\right)\to \left(\left(R\in \mathrm{Disjs}\wedge R\mathrm{DomainQss}A\right)\leftrightarrow \left(R\in \mathrm{Disjs}\wedge \mathrm{dom}R/R=A\right)\right)$$
5	2 4	bitrd	Could not format ( ( A e. V /\ R e. W ) -> ( R Parts A <-> ( R e. Disjs /\ ( dom R /. R ) = A ) ) ) : No typesetting found for |- ( ( A e. V /\ R e. W ) -> ( R Parts A <-> ( R e. Disjs /\ ( dom R /. R ) = A ) ) ) with typecode |-