Theorem ixpssmap2g

Description: An infinite Cartesian product is a subset of set exponentiation. This version of ixpssmapg avoids ax-rep . (Contributed by Mario Carneiro, 16-Nov-2014)

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

Proof

Step	Hyp	Ref	Expression
1		ixpf	$$⊢f\in \underset{x\in A}{⨉}B\to f:A⟶\bigcup _{x\in A}B$$
2	1	adantl	$$⊢\left(\bigcup _{x\in A}B\in V\wedge f\in \underset{x\in A}{⨉}B\right)\to f:A⟶\bigcup _{x\in A}B$$
3		n0i	$$⊢f\in \underset{x\in A}{⨉}B\to \neg \underset{x\in A}{⨉}B=\varnothing$$
4		ixpprc	$$⊢\neg A\in \mathrm{V}\to \underset{x\in A}{⨉}B=\varnothing$$
5	3 4	nsyl2	$$⊢f\in \underset{x\in A}{⨉}B\to A\in \mathrm{V}$$
6		elmapg	$$⊢\left(\bigcup _{x\in A}B\in V\wedge A\in \mathrm{V}\right)\to \left(f\in \left({\bigcup _{x\in A}B}^A\right)\leftrightarrow f:A⟶\bigcup _{x\in A}B\right)$$
7	5 6	sylan2	$$⊢\left(\bigcup _{x\in A}B\in V\wedge f\in \underset{x\in A}{⨉}B\right)\to \left(f\in \left({\bigcup _{x\in A}B}^A\right)\leftrightarrow f:A⟶\bigcup _{x\in A}B\right)$$
8	2 7	mpbird	$$⊢\left(\bigcup _{x\in A}B\in V\wedge f\in \underset{x\in A}{⨉}B\right)\to f\in \left({\bigcup _{x\in A}B}^A\right)$$
9	8	ex	$$⊢\bigcup _{x\in A}B\in V\to \left(f\in \underset{x\in A}{⨉}B\to f\in \left({\bigcup _{x\in A}B}^A\right)\right)$$
10	9	ssrdv	$$⊢\bigcup _{x\in A}B\in V\to \underset{x\in A}{⨉}B\subseteq {\bigcup _{x\in A}B}^A$$