Theorem ixpssmapg

Description: An infinite Cartesian product is a subset of set exponentiation. (Contributed by Jeff Madsen, 19-Jun-2011)

	Ref	Expression
Assertion	ixpssmapg	$$⊢\forall x\in AB\in V\to \underset{x\in A}{⨉}B\subseteq {\bigcup _{x\in A}B}^A$$

Proof

Step	Hyp	Ref	Expression
1		n0i	$$⊢f\in \underset{x\in A}{⨉}B\to \neg \underset{x\in A}{⨉}B=\varnothing$$
2		ixpprc	$$⊢\neg A\in \mathrm{V}\to \underset{x\in A}{⨉}B=\varnothing$$
3	1 2	nsyl2	$$⊢f\in \underset{x\in A}{⨉}B\to A\in \mathrm{V}$$
4		id	$$⊢\forall x\in AB\in V\to \forall x\in AB\in V$$
5		iunexg	$$⊢\left(A\in \mathrm{V}\wedge \forall x\in AB\in V\right)\to \bigcup _{x\in A}B\in \mathrm{V}$$
6	3 4 5	syl2anr	$$⊢\left(\forall x\in AB\in V\wedge f\in \underset{x\in A}{⨉}B\right)\to \bigcup _{x\in A}B\in \mathrm{V}$$
7		ixpssmap2g	$$⊢\bigcup _{x\in A}B\in \mathrm{V}\to \underset{x\in A}{⨉}B\subseteq {\bigcup _{x\in A}B}^A$$
8	6 7	syl	$$⊢\left(\forall x\in AB\in V\wedge f\in \underset{x\in A}{⨉}B\right)\to \underset{x\in A}{⨉}B\subseteq {\bigcup _{x\in A}B}^A$$
9		simpr	$$⊢\left(\forall x\in AB\in V\wedge f\in \underset{x\in A}{⨉}B\right)\to f\in \underset{x\in A}{⨉}B$$
10	8 9	sseldd	$$⊢\left(\forall x\in AB\in V\wedge f\in \underset{x\in A}{⨉}B\right)\to f\in \left({\bigcup _{x\in A}B}^A\right)$$
11	10	ex	$$⊢\forall x\in AB\in V\to \left(f\in \underset{x\in A}{⨉}B\to f\in \left({\bigcup _{x\in A}B}^A\right)\right)$$
12	11	ssrdv	$$⊢\forall x\in AB\in V\to \underset{x\in A}{⨉}B\subseteq {\bigcup _{x\in A}B}^A$$