xrninxpex

Description: Sufficient condition for the intersection of a range Cartesian product with a Cartesian product to be a set. (Contributed by Peter Mazsa, 12-Apr-2020)

		Ref	Expression
	Assertion	xrninxpex	$⊢ (A \in V \land B \in W \land C \in X) \to R ⋉ S \cap (A \times (B \times C)) \in V$

Proof

Step	Hyp	Ref	Expression
1		xpexg	$⊢ (B \in W \land C \in X) \to B \times C \in V$
2		inxpex	$⊢ (R ⋉ S \in V \lor (A \in V \land B \times C \in V)) \to R ⋉ S \cap (A \times (B \times C)) \in V$
3	2	olcs	$⊢ (A \in V \land B \times C \in V) \to R ⋉ S \cap (A \times (B \times C)) \in V$
4	1 3	sylan2	$⊢ (A \in V \land (B \in W \land C \in X)) \to R ⋉ S \cap (A \times (B \times C)) \in V$
5	4	3impb	$⊢ (A \in V \land B \in W \land C \in X) \to R ⋉ S \cap (A \times (B \times C)) \in V$

Metamath Proof Explorer

Theorem xrninxpex

Proof