Metamath Proof Explorer

Theorem petxrnidres2

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

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

Proof

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