Metamath Proof Explorer

Theorem ixpiin

Description: The indexed intersection of a collection of infinite Cartesian products. (Contributed by Mario Carneiro, 6-Feb-2015)

Ref Expression
Assertion ixpiin ⊢ B ≠ ∅ → ⨉ x ∈ A ⋂ y ∈ B C = ⋂ y ∈ B ⨉ x ∈ A C

Proof

Step Hyp Ref Expression
1 r19.28zv ⊢ B ≠ ∅ → ∀ y ∈ B f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ C ↔ f Fn A ∧ ∀ y ∈ B ∀ x ∈ A f ⁡ x ∈ C
2 eliin ⊢ f ∈ V → f ∈ ⋂ y ∈ B ⨉ x ∈ A C ↔ ∀ y ∈ B f ∈ ⨉ x ∈ A C
3 2 elv ⊢ f ∈ ⋂ y ∈ B ⨉ x ∈ A C ↔ ∀ y ∈ B f ∈ ⨉ x ∈ A C
4 vex ⊢ f ∈ V
5 4 elixp ⊢ f ∈ ⨉ x ∈ A C ↔ f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ C
6 5 ralbii ⊢ ∀ y ∈ B f ∈ ⨉ x ∈ A C ↔ ∀ y ∈ B f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ C
7 3 6 bitri ⊢ f ∈ ⋂ y ∈ B ⨉ x ∈ A C ↔ ∀ y ∈ B f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ C
8 4 elixp ⊢ f ∈ ⨉ x ∈ A ⋂ y ∈ B C ↔ f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ ⋂ y ∈ B C
9 fvex ⊢ f ⁡ x ∈ V
10 eliin ⊢ f ⁡ x ∈ V → f ⁡ x ∈ ⋂ y ∈ B C ↔ ∀ y ∈ B f ⁡ x ∈ C
11 9 10 ax-mp ⊢ f ⁡ x ∈ ⋂ y ∈ B C ↔ ∀ y ∈ B f ⁡ x ∈ C
12 11 ralbii ⊢ ∀ x ∈ A f ⁡ x ∈ ⋂ y ∈ B C ↔ ∀ x ∈ A ∀ y ∈ B f ⁡ x ∈ C
13 ralcom ⊢ ∀ x ∈ A ∀ y ∈ B f ⁡ x ∈ C ↔ ∀ y ∈ B ∀ x ∈ A f ⁡ x ∈ C
14 12 13 bitri ⊢ ∀ x ∈ A f ⁡ x ∈ ⋂ y ∈ B C ↔ ∀ y ∈ B ∀ x ∈ A f ⁡ x ∈ C
15 14 anbi2i ⊢ f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ ⋂ y ∈ B C ↔ f Fn A ∧ ∀ y ∈ B ∀ x ∈ A f ⁡ x ∈ C
16 8 15 bitri ⊢ f ∈ ⨉ x ∈ A ⋂ y ∈ B C ↔ f Fn A ∧ ∀ y ∈ B ∀ x ∈ A f ⁡ x ∈ C
17 1 7 16 3bitr4g ⊢ B ≠ ∅ → f ∈ ⋂ y ∈ B ⨉ x ∈ A C ↔ f ∈ ⨉ x ∈ A ⋂ y ∈ B C
18 17 eqrdv ⊢ B ≠ ∅ → ⋂ y ∈ B ⨉ x ∈ A C = ⨉ x ∈ A ⋂ y ∈ B C
19 18 eqcomd ⊢ B ≠ ∅ → ⨉ x ∈ A ⋂ y ∈ B C = ⋂ y ∈ B ⨉ x ∈ A C