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}) \land dom R ⋉ ({I ↾}_{A}) / R ⋉ ({I ↾}_{A}) = A) \leftrightarrow (EqvRel ≀ R ⋉ ({I ↾}_{A}) \land 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}) \land dom R ⋉ ({I ↾}_{A}) / R ⋉ ({I ↾}_{A}) = A) \leftrightarrow (EqvRel ≀ R ⋉ ({I ↾}_{A}) \land dom ≀ R ⋉ ({I ↾}_{A}) / ≀ R ⋉ ({I ↾}_{A}) = A)$