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 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 ( 𝑅 ∩ ( I ↾ 𝐴 ) ) ∧ ( dom ( 𝑅 ∩ ( I ↾ 𝐴 ) ) / ( 𝑅 ∩ ( I ↾ 𝐴 ) ) ) = 𝐴 ) ↔ ( EqvRel ≀ ( 𝑅 ∩ ( I ↾ 𝐴 ) ) ∧ ( dom ≀ ( 𝑅 ∩ ( I ↾ 𝐴 ) ) / ≀ ( 𝑅 ∩ ( I ↾ 𝐴 ) ) ) = 𝐴 ) )
Proof
Step
Hyp
Ref
Expression
1
disjALTVinidres ⊢ Disj ( 𝑅 ∩ ( I ↾ 𝐴 ) )
2
1
petlemi ⊢ ( ( Disj ( 𝑅 ∩ ( I ↾ 𝐴 ) ) ∧ ( dom ( 𝑅 ∩ ( I ↾ 𝐴 ) ) / ( 𝑅 ∩ ( I ↾ 𝐴 ) ) ) = 𝐴 ) ↔ ( EqvRel ≀ ( 𝑅 ∩ ( I ↾ 𝐴 ) ) ∧ ( dom ≀ ( 𝑅 ∩ ( I ↾ 𝐴 ) ) / ≀ ( 𝑅 ∩ ( I ↾ 𝐴 ) ) ) = 𝐴 ) )