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	⊢ 𝐴 ∈ V
		xpmapen.2	⊢ 𝐵 ∈ V
		xpmapen.3	⊢ 𝐶 ∈ V
	Assertion	xpmapen	⊢ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ≈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		xpmapen.1	⊢ 𝐴 ∈ V
2		xpmapen.2	⊢ 𝐵 ∈ V
3		xpmapen.3	⊢ 𝐶 ∈ V
4		2fveq3	⊢ ( 𝑤 = 𝑧 → ( 1^st ‘ ( 𝑥 ‘ 𝑤 ) ) = ( 1^st ‘ ( 𝑥 ‘ 𝑧 ) ) )
5	4	cbvmptv	⊢ ( 𝑤 ∈ 𝐶 ↦ ( 1^st ‘ ( 𝑥 ‘ 𝑤 ) ) ) = ( 𝑧 ∈ 𝐶 ↦ ( 1^st ‘ ( 𝑥 ‘ 𝑧 ) ) )
6		2fveq3	⊢ ( 𝑤 = 𝑧 → ( 2^nd ‘ ( 𝑥 ‘ 𝑤 ) ) = ( 2^nd ‘ ( 𝑥 ‘ 𝑧 ) ) )
7	6	cbvmptv	⊢ ( 𝑤 ∈ 𝐶 ↦ ( 2^nd ‘ ( 𝑥 ‘ 𝑤 ) ) ) = ( 𝑧 ∈ 𝐶 ↦ ( 2^nd ‘ ( 𝑥 ‘ 𝑧 ) ) )
8		fveq2	⊢ ( 𝑤 = 𝑧 → ( ( 1^st ‘ 𝑦 ) ‘ 𝑤 ) = ( ( 1^st ‘ 𝑦 ) ‘ 𝑧 ) )
9		fveq2	⊢ ( 𝑤 = 𝑧 → ( ( 2^nd ‘ 𝑦 ) ‘ 𝑤 ) = ( ( 2^nd ‘ 𝑦 ) ‘ 𝑧 ) )
10	8 9	opeq12d	⊢ ( 𝑤 = 𝑧 → ⟨ ( ( 1^st ‘ 𝑦 ) ‘ 𝑤 ) , ( ( 2^nd ‘ 𝑦 ) ‘ 𝑤 ) ⟩ = ⟨ ( ( 1^st ‘ 𝑦 ) ‘ 𝑧 ) , ( ( 2^nd ‘ 𝑦 ) ‘ 𝑧 ) ⟩ )
11	10	cbvmptv	⊢ ( 𝑤 ∈ 𝐶 ↦ ⟨ ( ( 1^st ‘ 𝑦 ) ‘ 𝑤 ) , ( ( 2^nd ‘ 𝑦 ) ‘ 𝑤 ) ⟩ ) = ( 𝑧 ∈ 𝐶 ↦ ⟨ ( ( 1^st ‘ 𝑦 ) ‘ 𝑧 ) , ( ( 2^nd ‘ 𝑦 ) ‘ 𝑧 ) ⟩ )
12	1 2 3 5 7 11	xpmapenlem	⊢ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ≈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) )