Theorem iunmapss

Description: The indexed union of set exponentiations is a subset of the set exponentiation of the indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	iunmapss.x	$$⊢Ⅎx\phi$$
	iunmapss.a	$$⊢\phi \to A\in V$$
	iunmapss.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in W$$
Assertion	iunmapss	$$⊢\phi \to \bigcup _{x\in A}\left(B^C\right)\subseteq {\bigcup _{x\in A}B}^C$$

Proof

Step	Hyp	Ref	Expression
1		iunmapss.x	$$⊢Ⅎx\phi$$
2		iunmapss.a	$$⊢\phi \to A\in V$$
3		iunmapss.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in W$$
4	3	ex	$$⊢\phi \to \left(x\in A\to B\in W\right)$$
5	1 4	ralrimi	$$⊢\phi \to \forall x\in AB\in W$$
6		iunexg	$$⊢\left(A\in V\wedge \forall x\in AB\in W\right)\to \bigcup _{x\in A}B\in \mathrm{V}$$
7	2 5 6	syl2anc	$$⊢\phi \to \bigcup _{x\in A}B\in \mathrm{V}$$
8	7	adantr	$$⊢\left(\phi \wedge x\in A\right)\to \bigcup _{x\in A}B\in \mathrm{V}$$
9		ssiun2	$$⊢x\in A\to B\subseteq \bigcup _{x\in A}B$$
10	9	adantl	$$⊢\left(\phi \wedge x\in A\right)\to B\subseteq \bigcup _{x\in A}B$$
11		mapss	$$⊢\left(\bigcup _{x\in A}B\in \mathrm{V}\wedge B\subseteq \bigcup _{x\in A}B\right)\to B^C\subseteq {\bigcup _{x\in A}B}^C$$
12	8 10 11	syl2anc	$$⊢\left(\phi \wedge x\in A\right)\to B^C\subseteq {\bigcup _{x\in A}B}^C$$
13	12	ex	$$⊢\phi \to \left(x\in A\to B^C\subseteq {\bigcup _{x\in A}B}^C\right)$$
14	1 13	ralrimi	$$⊢\phi \to \forall x\in A{B}^C\subseteq {\bigcup _{x\in A}B}^C$$
15		nfiu1	$$⊢\underset{\_}{Ⅎ}x\bigcup _{x\in A}B$$
16		nfcv	$$⊢\underset{\_}{Ⅎ}x{\uparrow }_{𝑚}$$
17		nfcv	$$⊢\underset{\_}{Ⅎ}xC$$
18	15 16 17	nfov	$$⊢\underset{\_}{Ⅎ}x\left({\bigcup _{x\in A}B}^C\right)$$
19	18	iunssf	$$⊢\bigcup _{x\in A}\left(B^C\right)\subseteq {\bigcup _{x\in A}B}^C\leftrightarrow \forall x\in A{B}^C\subseteq {\bigcup _{x\in A}B}^C$$
20	14 19	sylibr	$$⊢\phi \to \bigcup _{x\in A}\left(B^C\right)\subseteq {\bigcup _{x\in A}B}^C$$