Theorem iunxpssiun1

Description: Provide an upper bound for the indexed union of cartesian products. (Contributed by Thierry Arnoux, 13-Oct-2025)

	Ref	Expression
Hypothesis	iunxpssiun1.1	$$⊢\left(\phi \wedge x\in A\right)\to C\subseteq E$$
Assertion	iunxpssiun1	$$⊢\phi \to \bigcup _{x\in A}\left(B\times C\right)\subseteq \bigcup _{x\in A}B\times E$$

Proof

Step	Hyp	Ref	Expression
1		iunxpssiun1.1	$$⊢\left(\phi \wedge x\in A\right)\to C\subseteq E$$
2		ssiun2	$$⊢x\in A\to B\subseteq \bigcup _{x\in A}B$$
3	2	adantl	$$⊢\left(\phi \wedge x\in A\right)\to B\subseteq \bigcup _{x\in A}B$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}yB$$
5		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌B$$
6		csbeq1a	$$⊢x=y\to B=⦋y/x⦌B$$
7	4 5 6	cbviun	$$⊢\bigcup _{x\in A}B=\bigcup _{y\in A}⦋y/x⦌B$$
8	3 7	sseqtrdi	$$⊢\left(\phi \wedge x\in A\right)\to B\subseteq \bigcup _{y\in A}⦋y/x⦌B$$
9		xpss12	$$⊢\left(B\subseteq \bigcup _{y\in A}⦋y/x⦌B\wedge C\subseteq E\right)\to B\times C\subseteq \bigcup _{y\in A}⦋y/x⦌B\times E$$
10	8 1 9	syl2anc	$$⊢\left(\phi \wedge x\in A\right)\to B\times C\subseteq \bigcup _{y\in A}⦋y/x⦌B\times E$$
11	10	ralrimiva	$$⊢\phi \to \forall x\in AB\times C\subseteq \bigcup _{y\in A}⦋y/x⦌B\times E$$
12		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
13	12 5	nfiun	$$⊢\underset{\_}{Ⅎ}x\bigcup _{y\in A}⦋y/x⦌B$$
14		nfcv	$$⊢\underset{\_}{Ⅎ}xE$$
15	13 14	nfxp	$$⊢\underset{\_}{Ⅎ}x\left(\bigcup _{y\in A}⦋y/x⦌B\times E\right)$$
16	15	iunssf	$$⊢\bigcup _{x\in A}\left(B\times C\right)\subseteq \bigcup _{y\in A}⦋y/x⦌B\times E\leftrightarrow \forall x\in AB\times C\subseteq \bigcup _{y\in A}⦋y/x⦌B\times E$$
17	11 16	sylibr	$$⊢\phi \to \bigcup _{x\in A}\left(B\times C\right)\subseteq \bigcup _{y\in A}⦋y/x⦌B\times E$$
18	7	xpeq1i	$$⊢\bigcup _{x\in A}B\times E=\bigcup _{y\in A}⦋y/x⦌B\times E$$
19	17 18	sseqtrrdi	$$⊢\phi \to \bigcup _{x\in A}\left(B\times C\right)\subseteq \bigcup _{x\in A}B\times E$$