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	$$⊢\phi \to A\ne \varnothing$$
	intxp.2	$$⊢\left(\phi \wedge x\in A\right)\to x=\mathrm{dom}x\times \mathrm{ran}x$$
	intxp.3	$$⊢X=\bigcap _{x\in A}\mathrm{dom}x$$
	intxp.4	$$⊢Y=\bigcap _{x\in A}\mathrm{ran}x$$
Assertion	intxp	$$⊢\phi \to \bigcap A=X\times Y$$

Proof

Step	Hyp	Ref	Expression
1		intxp.1	$$⊢\phi \to A\ne \varnothing$$
2		intxp.2	$$⊢\left(\phi \wedge x\in A\right)\to x=\mathrm{dom}x\times \mathrm{ran}x$$
3		intxp.3	$$⊢X=\bigcap _{x\in A}\mathrm{dom}x$$
4		intxp.4	$$⊢Y=\bigcap _{x\in A}\mathrm{ran}x$$
5		intiin	$$⊢\bigcap A=\bigcap _{x\in A}x$$
6	2	iineq2dv	$$⊢\phi \to \bigcap _{x\in A}x=\bigcap _{x\in A}\left(\mathrm{dom}x\times \mathrm{ran}x\right)$$
7	5 6	eqtrid	$$⊢\phi \to \bigcap A=\bigcap _{x\in A}\left(\mathrm{dom}x\times \mathrm{ran}x\right)$$
8		iinxp	$$⊢A\ne \varnothing \to \bigcap _{x\in A}\left(\mathrm{dom}x\times \mathrm{ran}x\right)=\bigcap _{x\in A}\mathrm{dom}x\times \bigcap _{x\in A}\mathrm{ran}x$$
9	1 8	syl	$$⊢\phi \to \bigcap _{x\in A}\left(\mathrm{dom}x\times \mathrm{ran}x\right)=\bigcap _{x\in A}\mathrm{dom}x\times \bigcap _{x\in A}\mathrm{ran}x$$
10	7 9	eqtrd	$$⊢\phi \to \bigcap A=\bigcap _{x\in A}\mathrm{dom}x\times \bigcap _{x\in A}\mathrm{ran}x$$
11	3 4	xpeq12i	$$⊢X\times Y=\bigcap _{x\in A}\mathrm{dom}x\times \bigcap _{x\in A}\mathrm{ran}x$$
12	10 11	eqtr4di	$$⊢\phi \to \bigcap A=X\times Y$$