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 ( 𝐵 ≠ ∅ → X 𝑥𝐴 𝑦𝐵 𝐶 = 𝑦𝐵 X 𝑥𝐴 𝐶 )

Proof

Step Hyp Ref Expression
1 r19.28zv ( 𝐵 ≠ ∅ → ( ∀ 𝑦𝐵 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐶 ) ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑦𝐵𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐶 ) ) )
2 eliin ( 𝑓 ∈ V → ( 𝑓 𝑦𝐵 X 𝑥𝐴 𝐶 ↔ ∀ 𝑦𝐵 𝑓X 𝑥𝐴 𝐶 ) )
3 2 elv ( 𝑓 𝑦𝐵 X 𝑥𝐴 𝐶 ↔ ∀ 𝑦𝐵 𝑓X 𝑥𝐴 𝐶 )
4 vex 𝑓 ∈ V
5 4 elixp ( 𝑓X 𝑥𝐴 𝐶 ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐶 ) )
6 5 ralbii ( ∀ 𝑦𝐵 𝑓X 𝑥𝐴 𝐶 ↔ ∀ 𝑦𝐵 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐶 ) )
7 3 6 bitri ( 𝑓 𝑦𝐵 X 𝑥𝐴 𝐶 ↔ ∀ 𝑦𝐵 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐶 ) )
8 4 elixp ( 𝑓X 𝑥𝐴 𝑦𝐵 𝐶 ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝑦𝐵 𝐶 ) )
9 fvex ( 𝑓𝑥 ) ∈ V
10 eliin ( ( 𝑓𝑥 ) ∈ V → ( ( 𝑓𝑥 ) ∈ 𝑦𝐵 𝐶 ↔ ∀ 𝑦𝐵 ( 𝑓𝑥 ) ∈ 𝐶 ) )
11 9 10 ax-mp ( ( 𝑓𝑥 ) ∈ 𝑦𝐵 𝐶 ↔ ∀ 𝑦𝐵 ( 𝑓𝑥 ) ∈ 𝐶 )
12 11 ralbii ( ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝑦𝐵 𝐶 ↔ ∀ 𝑥𝐴𝑦𝐵 ( 𝑓𝑥 ) ∈ 𝐶 )
13 ralcom ( ∀ 𝑥𝐴𝑦𝐵 ( 𝑓𝑥 ) ∈ 𝐶 ↔ ∀ 𝑦𝐵𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐶 )
14 12 13 bitri ( ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝑦𝐵 𝐶 ↔ ∀ 𝑦𝐵𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐶 )
15 14 anbi2i ( ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝑦𝐵 𝐶 ) ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑦𝐵𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐶 ) )
16 8 15 bitri ( 𝑓X 𝑥𝐴 𝑦𝐵 𝐶 ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑦𝐵𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐶 ) )
17 1 7 16 3bitr4g ( 𝐵 ≠ ∅ → ( 𝑓 𝑦𝐵 X 𝑥𝐴 𝐶𝑓X 𝑥𝐴 𝑦𝐵 𝐶 ) )
18 17 eqrdv ( 𝐵 ≠ ∅ → 𝑦𝐵 X 𝑥𝐴 𝐶 = X 𝑥𝐴 𝑦𝐵 𝐶 )
19 18 eqcomd ( 𝐵 ≠ ∅ → X 𝑥𝐴 𝑦𝐵 𝐶 = 𝑦𝐵 X 𝑥𝐴 𝐶 )