Theorem intxpd

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	intxpd.1	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
	intxpd.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 = ( dom 𝑥 × ran 𝑥 ) )
	intxpd.3	⊢ 𝑋 = ∩ 𝑥 ∈ 𝐴 dom 𝑥
	intxpd.4	⊢ 𝑌 = ∩ 𝑥 ∈ 𝐴 ran 𝑥
Assertion	intxpd	⊢ ( 𝜑 → ∩ 𝐴 = ( 𝑋 × 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		intxpd.1	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
2		intxpd.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 = ( dom 𝑥 × ran 𝑥 ) )
3		intxpd.3	⊢ 𝑋 = ∩ 𝑥 ∈ 𝐴 dom 𝑥
4		intxpd.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	⊢ ( 𝜑 → ∩ 𝐴 = ( 𝑋 × 𝑌 ) )