Metamath Proof Explorer

Theorem petinidres

Description: A class is a partition by an intersection with the identity class restricted to it if and only if the cosets by the intersection are in equivalence relation on it. Cf. br1cossinidres , disjALTVinidres and eqvrel1cossinidres . (Contributed by Peter Mazsa, 31-Dec-2021)

Ref Expression
Assertion petinidres ⊢ R ∩ I ↾ A Part A ↔ ≀ R ∩ I ↾ A ErALTV A

Proof

Step Hyp Ref Expression
1 petinidres2 ⊢ 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