Theorem ixpssmap

Description: An infinite Cartesian product is a subset of set exponentiation. Remark in Enderton p. 54. (Contributed by NM, 28-Sep-2006)

	Ref	Expression
Hypothesis	ixpssmap.2	$$⊢B\in \mathrm{V}$$
Assertion	ixpssmap	$$⊢\underset{x\in A}{⨉}B\subseteq {\bigcup _{x\in A}B}^A$$

Proof

Step	Hyp	Ref	Expression
1		ixpssmap.2	$$⊢B\in \mathrm{V}$$
2	1	rgenw	$$⊢\forall x\in AB\in \mathrm{V}$$
3		ixpssmapg	$$⊢\forall x\in AB\in \mathrm{V}\to \underset{x\in A}{⨉}B\subseteq {\bigcup _{x\in A}B}^A$$
4	2 3	ax-mp	$$⊢\underset{x\in A}{⨉}B\subseteq {\bigcup _{x\in A}B}^A$$