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	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ⊆ 𝐸 )
Assertion	iunxpssiun1	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 ( 𝐵 × 𝐶 ) ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 × 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		iunxpssiun1.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ⊆ 𝐸 )
2		ssiun2	⊢ ( 𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
3	2	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
4		nfcv	⊢ Ⅎ 𝑦 𝐵
5		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
6		csbeq1a	⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
7	4 5 6	cbviun	⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
8	3 7	sseqtrdi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
9		xpss12	⊢ ( ( 𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∧ 𝐶 ⊆ 𝐸 ) → ( 𝐵 × 𝐶 ) ⊆ ( ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 × 𝐸 ) )
10	8 1 9	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 × 𝐶 ) ⊆ ( ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 × 𝐸 ) )
11	10	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝐵 × 𝐶 ) ⊆ ( ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 × 𝐸 ) )
12		nfcv	⊢ Ⅎ 𝑥 𝐴
13	12 5	nfiun	⊢ Ⅎ 𝑥 ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
14		nfcv	⊢ Ⅎ 𝑥 𝐸
15	13 14	nfxp	⊢ Ⅎ 𝑥 ( ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 × 𝐸 )
16	15	iunssf	⊢ ( ∪ 𝑥 ∈ 𝐴 ( 𝐵 × 𝐶 ) ⊆ ( ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 × 𝐸 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐵 × 𝐶 ) ⊆ ( ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 × 𝐸 ) )
17	11 16	sylibr	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 ( 𝐵 × 𝐶 ) ⊆ ( ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 × 𝐸 ) )
18	7	xpeq1i	⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 × 𝐸 ) = ( ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 × 𝐸 )
19	17 18	sseqtrrdi	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 ( 𝐵 × 𝐶 ) ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 × 𝐸 ) )