Theorem ixpconstg

Description: Infinite Cartesian product of a constant B . (Contributed by Mario Carneiro, 11-Jan-2015)

	Ref	Expression
Assertion	ixpconstg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → X 𝑥 ∈ 𝐴 𝐵 = ( 𝐵 ↑m 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑓 ∈ V
2	1	elixpconst	⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ↔ 𝑓 : 𝐴 ⟶ 𝐵 )
3	2	abbi2i	⊢ X 𝑥 ∈ 𝐴 𝐵 = { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 }
4		mapvalg	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐵 ↑m 𝐴 ) = { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } )
5	3 4	eqtr4id	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ) → X 𝑥 ∈ 𝐴 𝐵 = ( 𝐵 ↑m 𝐴 ) )
6	5	ancoms	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → X 𝑥 ∈ 𝐴 𝐵 = ( 𝐵 ↑m 𝐴 ) )