Theorem fprodxp

Description: Combine two products into a single product over the cartesian product. (Contributed by Scott Fenton, 1-Feb-2018)

	Ref	Expression
Hypotheses	fprodxp.1	$$⊢z=⟨j,k⟩\to D=C$$
	fprodxp.2	$$⊢\phi \to A\in \mathrm{Fin}$$
	fprodxp.3	$$⊢\phi \to B\in \mathrm{Fin}$$
	fprodxp.4	$$⊢\left(\phi \wedge \left(j\in A\wedge k\in B\right)\right)\to C\in ℂ$$
Assertion	fprodxp	$$⊢\phi \to \prod _{j\in A}\prod _{k\in B}C=\prod _{z\in A\times B}D$$

Proof

Step	Hyp	Ref	Expression
1		fprodxp.1	$$⊢z=⟨j,k⟩\to D=C$$
2		fprodxp.2	$$⊢\phi \to A\in \mathrm{Fin}$$
3		fprodxp.3	$$⊢\phi \to B\in \mathrm{Fin}$$
4		fprodxp.4	$$⊢\left(\phi \wedge \left(j\in A\wedge k\in B\right)\right)\to C\in ℂ$$
5	3	adantr	$$⊢\left(\phi \wedge j\in A\right)\to B\in \mathrm{Fin}$$
6	1 2 5 4	fprod2d	$$⊢\phi \to \prod _{j\in A}\prod _{k\in B}C=\prod _{z\in \bigcup _{j\in A}\left(\left\{j\right\}\times B\right)}D$$
7		iunxpconst	$$⊢\bigcup _{j\in A}\left(\left\{j\right\}\times B\right)=A\times B$$
8	7	prodeq1i	$$⊢\prod _{z\in \bigcup _{j\in A}\left(\left\{j\right\}\times B\right)}D=\prod _{z\in A\times B}D$$
9	6 8	syl6eq	$$⊢\phi \to \prod _{j\in A}\prod _{k\in B}C=\prod _{z\in A\times B}D$$