Metamath Proof Explorer


Theorem mpets2

Description: Member Partition-Equivalence Theorem with binary relations, cf. mpet2 . (Contributed by Peter Mazsa, 24-Sep-2021)

Ref Expression
Assertion mpets2 A V E -1 A Parts A E -1 A Ers A

Proof

Step Hyp Ref Expression
1 mpet2 E -1 A Part A E -1 A ErALTV A
2 cnvepresex A V E -1 A V
3 brpartspart A V E -1 A V E -1 A Parts A E -1 A Part A
4 2 3 mpdan A V E -1 A Parts A E -1 A Part A
5 1cosscnvepresex A V E -1 A V
6 brerser A V E -1 A V E -1 A Ers A E -1 A ErALTV A
7 5 6 mpdan A V E -1 A Ers A E -1 A ErALTV A
8 4 7 bibi12d A V E -1 A Parts A E -1 A Ers A E -1 A Part A E -1 A ErALTV A
9 1 8 mpbiri A V E -1 A Parts A E -1 A Ers A