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	|- ( ph -> A =/= (/) )
	intxp.2	|- ( ( ph /\ x e. A ) -> x = ( dom x X. ran x ) )
	intxp.3	|- X = |^|_ x e. A dom x
	intxp.4	|- Y = |^|_ x e. A ran x
Assertion	intxp	|- ( ph -> |^| A = ( X X. Y ) )

Proof

Step	Hyp	Ref	Expression
1		intxp.1	|- ( ph -> A =/= (/) )
2		intxp.2	|- ( ( ph /\ x e. A ) -> x = ( dom x X. ran x ) )
3		intxp.3	|- X = |^|_ x e. A dom x
4		intxp.4	|- Y = |^|_ x e. A ran x
5		intiin	|- |^| A = |^|_ x e. A x
6	2	iineq2dv	|- ( ph -> |^|_ x e. A x = |^|_ x e. A ( dom x X. ran x ) )
7	5 6	eqtrid	|- ( ph -> |^| A = |^|_ x e. A ( dom x X. ran x ) )
8		iinxp	|- ( A =/= (/) -> |^|_ x e. A ( dom x X. ran x ) = ( |^|_ x e. A dom x X. |^|_ x e. A ran x ) )
9	1 8	syl	|- ( ph -> |^|_ x e. A ( dom x X. ran x ) = ( |^|_ x e. A dom x X. |^|_ x e. A ran x ) )
10	7 9	eqtrd	|- ( ph -> |^| A = ( |^|_ x e. A dom x X. |^|_ x e. A ran x ) )
11	3 4	xpeq12i	|- ( X X. Y ) = ( |^|_ x e. A dom x X. |^|_ x e. A ran x )
12	10 11	eqtr4di	|- ( ph -> |^| A = ( X X. Y ) )