Theorem 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	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝑅 ⋉ 𝑆 ) ∩ ( 𝐴 × ( 𝐵 × 𝐶 ) ) ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		xpexg	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐵 × 𝐶 ) ∈ V )
2		inxpex	⊢ ( ( ( 𝑅 ⋉ 𝑆 ) ∈ V ∨ ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 × 𝐶 ) ∈ V ) ) → ( ( 𝑅 ⋉ 𝑆 ) ∩ ( 𝐴 × ( 𝐵 × 𝐶 ) ) ) ∈ V )
3	2	olcs	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 × 𝐶 ) ∈ V ) → ( ( 𝑅 ⋉ 𝑆 ) ∩ ( 𝐴 × ( 𝐵 × 𝐶 ) ) ) ∈ V )
4	1 3	sylan2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝑅 ⋉ 𝑆 ) ∩ ( 𝐴 × ( 𝐵 × 𝐶 ) ) ) ∈ V )
5	4	3impb	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝑅 ⋉ 𝑆 ) ∩ ( 𝐴 × ( 𝐵 × 𝐶 ) ) ) ∈ V )