This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 V$
		xpmapen.2	$⊢ B \in V$
		xpmapen.3	$⊢ C \in V$
	Assertion	xpmapen	$⊢ ({(A \times B)}^{C}) \approx ((A^{C}) \times (B^{C}))$

Proof

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