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