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

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 𝑥 ∈ 𝐴 𝐶 )