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∈BC=⋂y∈B⨉x∈AC

Proof

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