Metamath Proof Explorer

Theorem xrncnvepresex

Description: Sufficient condition for a range Cartesian product with restricted converse epsilon to be a set. (Contributed by Peter Mazsa, 16-Dec-2020) (Revised by Peter Mazsa, 23-Sep-2021)

		Ref	Expression
	Assertion	xrncnvepresex	$⊢ (A \in V \land R \in W) \to R ⋉ ({E^{-1} ↾}_{A}) \in V$

Proof

Step	Hyp	Ref	Expression
1		cnvepresex	$⊢ A \in V \to {E^{-1} ↾}_{A} \in V$
2	1	adantr	$⊢ (A \in V \land R \in W) \to {E^{-1} ↾}_{A} \in V$
3		xrnresex	$⊢ (A \in V \land R \in W \land {E^{-1} ↾}_{A} \in V) \to R ⋉ ({E^{-1} ↾}_{A}) \in V$
4	2 3	mpd3an3	$⊢ (A \in V \land R \in W) \to R ⋉ ({E^{-1} ↾}_{A}) \in V$