Theorem intxp

Description: Intersection of Cartesian products is the Cartesian product of intersection of domains and ranges. See also inxp and iinxp . (Contributed by Zhi Wang, 30-Oct-2025)

	Ref	Expression
Hypotheses	intxp.1	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
	intxp.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 = ( dom 𝑥 × ran 𝑥 ) )
	intxp.3	⊢ 𝑋 = ∩ 𝑥 ∈ 𝐴 dom 𝑥
	intxp.4	⊢ 𝑌 = ∩ 𝑥 ∈ 𝐴 ran 𝑥
Assertion	intxp	⊢ ( 𝜑 → ∩ 𝐴 = ( 𝑋 × 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		intxp.1	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
2		intxp.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 = ( dom 𝑥 × ran 𝑥 ) )
3		intxp.3	⊢ 𝑋 = ∩ 𝑥 ∈ 𝐴 dom 𝑥
4		intxp.4	⊢ 𝑌 = ∩ 𝑥 ∈ 𝐴 ran 𝑥
5		intiin	⊢ ∩ 𝐴 = ∩ 𝑥 ∈ 𝐴 𝑥
6	2	iineq2dv	⊢ ( 𝜑 → ∩ 𝑥 ∈ 𝐴 𝑥 = ∩ 𝑥 ∈ 𝐴 ( dom 𝑥 × ran 𝑥 ) )
7	5 6	eqtrid	⊢ ( 𝜑 → ∩ 𝐴 = ∩ 𝑥 ∈ 𝐴 ( dom 𝑥 × ran 𝑥 ) )
8		iinxp	⊢ ( 𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 ( dom 𝑥 × ran 𝑥 ) = ( ∩ 𝑥 ∈ 𝐴 dom 𝑥 × ∩ 𝑥 ∈ 𝐴 ran 𝑥 ) )
9	1 8	syl	⊢ ( 𝜑 → ∩ 𝑥 ∈ 𝐴 ( dom 𝑥 × ran 𝑥 ) = ( ∩ 𝑥 ∈ 𝐴 dom 𝑥 × ∩ 𝑥 ∈ 𝐴 ran 𝑥 ) )
10	7 9	eqtrd	⊢ ( 𝜑 → ∩ 𝐴 = ( ∩ 𝑥 ∈ 𝐴 dom 𝑥 × ∩ 𝑥 ∈ 𝐴 ran 𝑥 ) )
11	3 4	xpeq12i	⊢ ( 𝑋 × 𝑌 ) = ( ∩ 𝑥 ∈ 𝐴 dom 𝑥 × ∩ 𝑥 ∈ 𝐴 ran 𝑥 )
12	10 11	eqtr4di	⊢ ( 𝜑 → ∩ 𝐴 = ( 𝑋 × 𝑌 ) )