Metamath Proof Explorer

Theorem pet2

Description: Partition-Equivalence Theorem, with general R . This theorem (together with pet and pets ) is the main result of my investigation into set theory, see the comment of pet . (Contributed by Peter Mazsa, 24-May-2021) (Revised by Peter Mazsa, 23-Sep-2021)

Ref Expression
Assertion pet2 ⊢ Disj R ⋉ E -1 ↾ A ∧ dom ⁡ R ⋉ E -1 ↾ A / R ⋉ E -1 ↾ A = A ↔ EqvRel ≀ R ⋉ E -1 ↾ A ∧ dom ⁡ ≀ R ⋉ E -1 ↾ A / ≀ R ⋉ E -1 ↾ A = A

Proof

Step Hyp Ref Expression
1 eqvrelqseqdisj5 ⊢ EqvRel ≀ R ⋉ E -1 ↾ A ∧ dom ⁡ ≀ R ⋉ E -1 ↾ A / ≀ R ⋉ E -1 ↾ A = A → Disj R ⋉ E -1 ↾ A
2 1 petlem ⊢ Disj R ⋉ E -1 ↾ A ∧ dom ⁡ R ⋉ E -1 ↾ A / R ⋉ E -1 ↾ A = A ↔ EqvRel ≀ R ⋉ E -1 ↾ A ∧ dom ⁡ ≀ R ⋉ E -1 ↾ A / ≀ R ⋉ E -1 ↾ A = A