This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database SUPPLEMENTARY MATERIAL (USERS' MATHBOXES) Mathbox for Peter Mazsa Partition-Equivalence Theorems 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 ( 𝑅 ⋉ ( I ↾ 𝐴 ) ) ∧ ( dom ( 𝑅 ⋉ ( I ↾ 𝐴 ) ) / ( 𝑅 ⋉ ( I ↾ 𝐴 ) ) ) = 𝐴 ) ↔ ( EqvRel ≀ ( 𝑅 ⋉ ( I ↾ 𝐴 ) ) ∧ ( dom ≀ ( 𝑅 ⋉ ( I ↾ 𝐴 ) ) / ≀ ( 𝑅 ⋉ ( I ↾ 𝐴 ) ) ) = 𝐴 ) )
Proof
Step
Hyp
Ref
Expression
1
disjALTVxrnidres ⊢ Disj ( 𝑅 ⋉ ( I ↾ 𝐴 ) )
2
1
petlemi ⊢ ( ( Disj ( 𝑅 ⋉ ( I ↾ 𝐴 ) ) ∧ ( dom ( 𝑅 ⋉ ( I ↾ 𝐴 ) ) / ( 𝑅 ⋉ ( I ↾ 𝐴 ) ) ) = 𝐴 ) ↔ ( EqvRel ≀ ( 𝑅 ⋉ ( I ↾ 𝐴 ) ) ∧ ( dom ≀ ( 𝑅 ⋉ ( I ↾ 𝐴 ) ) / ≀ ( 𝑅 ⋉ ( I ↾ 𝐴 ) ) ) = 𝐴 ) )