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