Description: Member Partition-Equivalence Theorem in its shortest possible form: it shows that member partitions and comember equivalence relations are literally the same. Cf. pet , the Partition-Equivalence Theorem, with general R . (Contributed by Peter Mazsa, 31-Dec-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | mpets | |- MembParts = CoMembErs |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mpets2 | |- ( a e. _V -> ( ( `' _E |` a ) Parts a <-> ,~ ( `' _E |` a ) Ers a ) ) |
|
| 2 | 1 | elv | |- ( ( `' _E |` a ) Parts a <-> ,~ ( `' _E |` a ) Ers a ) |
| 3 | 2 | abbii | |- { a | ( `' _E |` a ) Parts a } = { a | ,~ ( `' _E |` a ) Ers a } |
| 4 | df-membparts | |- MembParts = { a | ( `' _E |` a ) Parts a } |
|
| 5 | df-comembers | |- CoMembErs = { a | ,~ ( `' _E |` a ) Ers a } |
|
| 6 | 3 4 5 | 3eqtr4i | |- MembParts = CoMembErs |