Metamath Proof Explorer

Theorem iinxp

Description: Indexed intersection of Cartesian products is the Cartesian product of indexed intersections. See also inxp and intxp . (Contributed by Zhi Wang, 30-Oct-2025)

Ref Expression
Assertion iinxp ⊢ A ≠ ∅ → ⋂ x ∈ A B × C = ⋂ x ∈ A B × ⋂ x ∈ A C

Proof

Step Hyp Ref Expression
1 relxp ⊢ Rel ⁡ B × C
2 1 rgenw ⊢ ∀ x ∈ A Rel ⁡ B × C
3 r19.2z ⊢ A ≠ ∅ ∧ ∀ x ∈ A Rel ⁡ B × C → ∃ x ∈ A Rel ⁡ B × C
4 2 3 mpan2 ⊢ A ≠ ∅ → ∃ x ∈ A Rel ⁡ B × C
5 reliin ⊢ ∃ x ∈ A Rel ⁡ B × C → Rel ⁡ ⋂ x ∈ A B × C
6 4 5 syl ⊢ A ≠ ∅ → Rel ⁡ ⋂ x ∈ A B × C
7 relxp ⊢ Rel ⁡ ⋂ x ∈ A B × ⋂ x ∈ A C
8 eliin ⊢ y ∈ V → y ∈ ⋂ x ∈ A B ↔ ∀ x ∈ A y ∈ B
9 8 elv ⊢ y ∈ ⋂ x ∈ A B ↔ ∀ x ∈ A y ∈ B
10 eliin ⊢ z ∈ V → z ∈ ⋂ x ∈ A C ↔ ∀ x ∈ A z ∈ C
11 10 elv ⊢ z ∈ ⋂ x ∈ A C ↔ ∀ x ∈ A z ∈ C
12 9 11 anbi12i ⊢ y ∈ ⋂ x ∈ A B ∧ z ∈ ⋂ x ∈ A C ↔ ∀ x ∈ A y ∈ B ∧ ∀ x ∈ A z ∈ C
13 opelxp ⊢ y z ∈ ⋂ x ∈ A B × ⋂ x ∈ A C ↔ y ∈ ⋂ x ∈ A B ∧ z ∈ ⋂ x ∈ A C
14 opex ⊢ y z ∈ V
15 eliin ⊢ y z ∈ V → y z ∈ ⋂ x ∈ A B × C ↔ ∀ x ∈ A y z ∈ B × C
16 14 15 ax-mp ⊢ y z ∈ ⋂ x ∈ A B × C ↔ ∀ x ∈ A y z ∈ B × C
17 opelxp ⊢ y z ∈ B × C ↔ y ∈ B ∧ z ∈ C
18 17 ralbii ⊢ ∀ x ∈ A y z ∈ B × C ↔ ∀ x ∈ A y ∈ B ∧ z ∈ C
19 r19.26 ⊢ ∀ x ∈ A y ∈ B ∧ z ∈ C ↔ ∀ x ∈ A y ∈ B ∧ ∀ x ∈ A z ∈ C
20 16 18 19 3bitri ⊢ y z ∈ ⋂ x ∈ A B × C ↔ ∀ x ∈ A y ∈ B ∧ ∀ x ∈ A z ∈ C
21 12 13 20 3bitr4ri ⊢ y z ∈ ⋂ x ∈ A B × C ↔ y z ∈ ⋂ x ∈ A B × ⋂ x ∈ A C
22 21 eqrelriv ⊢ Rel ⁡ ⋂ x ∈ A B × C ∧ Rel ⁡ ⋂ x ∈ A B × ⋂ x ∈ A C → ⋂ x ∈ A B × C = ⋂ x ∈ A B × ⋂ x ∈ A C
23 6 7 22 sylancl ⊢ A ≠ ∅ → ⋂ x ∈ A B × C = ⋂ x ∈ A B × ⋂ x ∈ A C