This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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