Metamath Proof Explorer

Theorem pets

Description: Partition-Equivalence Theorem with general R , with binary relations. This theorem (together with pet and pet2 ) is the main result of my investigation into set theory, cf. the comment of pet . (Contributed by Peter Mazsa, 23-Sep-2021)

Ref Expression
Assertion pets 
|- ( ( A e. V /\ R e. W ) -> ( ( R |X. ( `' _E |` A ) ) Parts A <-> ,~ ( R |X. ( `' _E |` A ) ) Ers A ) )

Proof

Step Hyp Ref Expression
1 pet 
 |-  ( ( R |X. ( `' _E |` A ) ) Part A <-> ,~ ( R |X. ( `' _E |` A ) ) ErALTV A )
2 xrncnvepresex 
 |-  ( ( A e. V /\ R e. W ) -> ( R |X. ( `' _E |` A ) ) e. _V )
3 brpartspart 
 |-  ( ( A e. V /\ ( R |X. ( `' _E |` A ) ) e. _V ) -> ( ( R |X. ( `' _E |` A ) ) Parts A <-> ( R |X. ( `' _E |` A ) ) Part A ) )
4 2 3 syldan 
 |-  ( ( A e. V /\ R e. W ) -> ( ( R |X. ( `' _E |` A ) ) Parts A <-> ( R |X. ( `' _E |` A ) ) Part A ) )
5 1cossxrncnvepresex 
 |-  ( ( A e. V /\ R e. W ) -> ,~ ( R |X. ( `' _E |` A ) ) e. _V )
6 brerser 
 |-  ( ( A e. V /\ ,~ ( R |X. ( `' _E |` A ) ) e. _V ) -> ( ,~ ( R |X. ( `' _E |` A ) ) Ers A <-> ,~ ( R |X. ( `' _E |` A ) ) ErALTV A ) )
7 5 6 syldan 
 |-  ( ( A e. V /\ R e. W ) -> ( ,~ ( R |X. ( `' _E |` A ) ) Ers A <-> ,~ ( R |X. ( `' _E |` A ) ) ErALTV A ) )
8 4 7 bibi12d 
 |-  ( ( A e. V /\ R e. W ) -> ( ( ( R |X. ( `' _E |` A ) ) Parts A <-> ,~ ( R |X. ( `' _E |` A ) ) Ers A ) <-> ( ( R |X. ( `' _E |` A ) ) Part A <-> ,~ ( R |X. ( `' _E |` A ) ) ErALTV A ) ) )
9 1 8 mpbiri 
 |-  ( ( A e. V /\ R e. W ) -> ( ( R |X. ( `' _E |` A ) ) Parts A <-> ,~ ( R |X. ( `' _E |` A ) ) Ers A ) )