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	$⊢ (φ \land x \in A) \to C \subseteq E$
	Assertion	iunxpssiun1	$⊢ φ \to ⋃_{x \in A} (B \times C) \subseteq ⋃_{x \in A} B \times E$

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

Metamath Proof Explorer