Metamath Proof Explorer

Theorem petxrnidres

Description: A class is a partition by a range Cartesian product with the identity class restricted to it if and only if the cosets by the range Cartesian product are in equivalence relation on it. Cf. br1cossxrnidres , disjALTVxrnidres and eqvrel1cossxrnidres . (Contributed by Peter Mazsa, 31-Dec-2021)

Ref Expression
Assertion petxrnidres ⊢ R ⋉ I ↾ A Part A ↔ ≀ R ⋉ I ↾ A ErALTV A

Proof

Step Hyp Ref Expression
1 petxrnidres2 ⊢ Disj R ⋉ I ↾ A ∧ dom ⁡ R ⋉ I ↾ A / R ⋉ I ↾ A = A ↔ EqvRel ≀ R ⋉ I ↾ A ∧ dom ⁡ ≀ R ⋉ I ↾ A / ≀ R ⋉ I ↾ A = A
2 dfpart2 ⊢ R ⋉ I ↾ A Part A ↔ Disj R ⋉ I ↾ A ∧ dom ⁡ R ⋉ I ↾ A / R ⋉ I ↾ A = A
3 dferALTV2 ⊢ ≀ R ⋉ I ↾ A ErALTV A ↔ EqvRel ≀ R ⋉ I ↾ A ∧ dom ⁡ ≀ R ⋉ I ↾ A / ≀ R ⋉ I ↾ A = A
4 1 2 3 3bitr4i ⊢ R ⋉ I ↾ A Part A ↔ ≀ R ⋉ I ↾ A ErALTV A