This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem petinidres2

Description: Class A 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. (Contributed by Peter Mazsa, 31-Dec-2021)

Ref Expression
Assertion 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

Proof

Step Hyp Ref Expression
1 disjALTVinidres ⊢ Disj R ∩ I ↾ A
2 1 petlemi ⊢ Disj R ∩ I ↾ A ∧ dom ⁡ R ∩ I ↾ A / R ∩ I ↾ A = A ↔ EqvRel ≀ R ∩ I ↾ A ∧ dom ⁡ ≀ R ∩ I ↾ A / ≀ R ∩ I ↾ A = A