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 ∈ V ∧ R ∈ W → R ⋉ E -1 ↾ A Parts A ↔ ≀ R ⋉ E -1 ↾ A Ers A

Proof

Step Hyp Ref Expression
1 pet ⊢ R ⋉ E -1 ↾ A Part A ↔ ≀ R ⋉ E -1 ↾ A ErALTV A
2 xrncnvepresex ⊢ A ∈ V ∧ R ∈ W → R ⋉ E -1 ↾ A ∈ V
3 brpartspart ⊢ A ∈ V ∧ R ⋉ E -1 ↾ A ∈ V → R ⋉ E -1 ↾ A Parts A ↔ R ⋉ E -1 ↾ A Part A
4 2 3 syldan ⊢ A ∈ V ∧ R ∈ W → R ⋉ E -1 ↾ A Parts A ↔ R ⋉ E -1 ↾ A Part A
5 1cossxrncnvepresex ⊢ A ∈ V ∧ R ∈ W → ≀ R ⋉ E -1 ↾ A ∈ V
6 brerser ⊢ A ∈ V ∧ ≀ R ⋉ E -1 ↾ A ∈ V → ≀ R ⋉ E -1 ↾ A Ers A ↔ ≀ R ⋉ E -1 ↾ A ErALTV A
7 5 6 syldan ⊢ A ∈ V ∧ R ∈ W → ≀ R ⋉ E -1 ↾ A Ers A ↔ ≀ R ⋉ E -1 ↾ A ErALTV A
8 4 7 bibi12d ⊢ A ∈ V ∧ R ∈ W → R ⋉ E -1 ↾ A Parts A ↔ ≀ R ⋉ E -1 ↾ A Ers A ↔ R ⋉ E -1 ↾ A Part A ↔ ≀ R ⋉ E -1 ↾ A ErALTV A
9 1 8 mpbiri ⊢ A ∈ V ∧ R ∈ W → R ⋉ E -1 ↾ A Parts A ↔ ≀ R ⋉ E -1 ↾ A Ers A