Theorem ixpssmapc

Description: An infinite Cartesian product is a subset of set exponentiation. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	ixpssmapc.x	$$⊢Ⅎx\phi$$
	ixpssmapc.c	$$⊢\phi \to C\in V$$
	ixpssmapc.b	$$⊢\left(\phi \wedge x\in A\right)\to B\subseteq C$$
Assertion	ixpssmapc	$$⊢\phi \to \underset{x\in A}{⨉}B\subseteq C^A$$

Proof

Step	Hyp	Ref	Expression
1		ixpssmapc.x	$$⊢Ⅎx\phi$$
2		ixpssmapc.c	$$⊢\phi \to C\in V$$
3		ixpssmapc.b	$$⊢\left(\phi \wedge x\in A\right)\to B\subseteq C$$
4	3	ex	$$⊢\phi \to \left(x\in A\to B\subseteq C\right)$$
5	1 4	ralrimi	$$⊢\phi \to \forall x\in AB\subseteq C$$
6		iunss	$$⊢\bigcup _{x\in A}B\subseteq C\leftrightarrow \forall x\in AB\subseteq C$$
7	5 6	sylibr	$$⊢\phi \to \bigcup _{x\in A}B\subseteq C$$
8	2 7	ssexd	$$⊢\phi \to \bigcup _{x\in A}B\in \mathrm{V}$$
9		ixpssmap2g	$$⊢\bigcup _{x\in A}B\in \mathrm{V}\to \underset{x\in A}{⨉}B\subseteq {\bigcup _{x\in A}B}^A$$
10	8 9	syl	$$⊢\phi \to \underset{x\in A}{⨉}B\subseteq {\bigcup _{x\in A}B}^A$$
11		mapss	$$⊢\left(C\in V\wedge \bigcup _{x\in A}B\subseteq C\right)\to {\bigcup _{x\in A}B}^A\subseteq C^A$$
12	2 7 11	syl2anc	$$⊢\phi \to {\bigcup _{x\in A}B}^A\subseteq C^A$$
13	10 12	sstrd	$$⊢\phi \to \underset{x\in A}{⨉}B\subseteq C^A$$