Theorem xpmapen

Description: Equinumerosity law for set exponentiation of a Cartesian product. Exercise 4.47 of Mendelson p. 255. (Contributed by NM, 23-Feb-2004) (Proof shortened by Mario Carneiro, 16-Nov-2014)

	Ref	Expression
Hypotheses	xpmapen.1	$$⊢A\in \mathrm{V}$$
	xpmapen.2	$$⊢B\in \mathrm{V}$$
	xpmapen.3	$$⊢C\in \mathrm{V}$$
Assertion	xpmapen	$$⊢\left({\left(A\times B\right)}^C\right)\approx \left(\left(A^C\right)\times \left(B^C\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		xpmapen.1	$$⊢A\in \mathrm{V}$$
2		xpmapen.2	$$⊢B\in \mathrm{V}$$
3		xpmapen.3	$$⊢C\in \mathrm{V}$$
4		2fveq3	$$⊢w=z\to 1^{st}\left(x\left(w\right)\right)=1^{st}\left(x\left(z\right)\right)$$
5	4	cbvmptv	$$⊢\left(w\in C⟼1^{st}\left(x\left(w\right)\right)\right)=\left(z\in C⟼1^{st}\left(x\left(z\right)\right)\right)$$
6		2fveq3	$$⊢w=z\to 2^{nd}\left(x\left(w\right)\right)=2^{nd}\left(x\left(z\right)\right)$$
7	6	cbvmptv	$$⊢\left(w\in C⟼2^{nd}\left(x\left(w\right)\right)\right)=\left(z\in C⟼2^{nd}\left(x\left(z\right)\right)\right)$$
8		fveq2	$$⊢w=z\to 1^{st}\left(y\right)\left(w\right)=1^{st}\left(y\right)\left(z\right)$$
9		fveq2	$$⊢w=z\to 2^{nd}\left(y\right)\left(w\right)=2^{nd}\left(y\right)\left(z\right)$$
10	8 9	opeq12d	$$⊢w=z\to ⟨1^{st}\left(y\right)\left(w\right),2^{nd}\left(y\right)\left(w\right)⟩=⟨1^{st}\left(y\right)\left(z\right),2^{nd}\left(y\right)\left(z\right)⟩$$
11	10	cbvmptv	$$⊢\left(w\in C⟼⟨1^{st}\left(y\right)\left(w\right),2^{nd}\left(y\right)\left(w\right)⟩\right)=\left(z\in C⟼⟨1^{st}\left(y\right)\left(z\right),2^{nd}\left(y\right)\left(z\right)⟩\right)$$
12	1 2 3 5 7 11	xpmapenlem	$$⊢\left({\left(A\times B\right)}^C\right)\approx \left(\left(A^C\right)\times \left(B^C\right)\right)$$