Description: Partition with general R (in addition to the member partition cf. mpet and mpet2 ) implies equivalent comembers. (Contributed by Peter Mazsa, 23-Sep-2021) (Revised by Peter Mazsa, 22-Dec-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | partimcomember | |- ( R Part A -> CoMembEr A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | partim | |- ( R Part A -> ,~ R ErALTV A ) |
|
| 2 | mainer | |- ( ,~ R ErALTV A -> CoMembEr A ) |
|
| 3 | 1 2 | syl | |- ( R Part A -> CoMembEr A ) |