This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 
|- ( ( A e. V /\ R e. W ) -> ( R Parts A <-> R Part A ) )

Proof

Step Hyp Ref Expression
1 eldisjsdisj 
 |-  ( R e. W -> ( R e. Disjs <-> Disj R ) )
2 1 adantl 
 |-  ( ( A e. V /\ R e. W ) -> ( R e. Disjs <-> Disj R ) )
3 brdmqssqs 
 |-  ( ( A e. V /\ R e. W ) -> ( R DomainQss A <-> R DomainQs A ) )
4 2 3 anbi12d 
 |-  ( ( A e. V /\ R e. W ) -> ( ( R e. Disjs /\ R DomainQss A ) <-> ( Disj R /\ R DomainQs A ) ) )
5 brparts 
 |-  ( A e. V -> ( R Parts A <-> ( R e. Disjs /\ R DomainQss A ) ) )
6 5 adantr 
 |-  ( ( A e. V /\ R e. W ) -> ( R Parts A <-> ( R e. Disjs /\ R DomainQss A ) ) )
7 df-part 
 |-  ( R Part A <-> ( Disj R /\ R DomainQs A ) )
8 7 a1i 
 |-  ( ( A e. V /\ R e. W ) -> ( R Part A <-> ( Disj R /\ R DomainQs A ) ) )
9 4 6 8 3bitr4d 
 |-  ( ( A e. V /\ R e. W ) -> ( R Parts A <-> R Part A ) )