Theorem ixpin

Description: The intersection of two infinite Cartesian products. (Contributed by Mario Carneiro, 3-Feb-2015)

	Ref	Expression
Assertion	ixpin	⊢ X 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) = ( X 𝑥 ∈ 𝐴 𝐵 ∩ X 𝑥 ∈ 𝐴 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		anandi	⊢ ( ( 𝑓 Fn 𝐴 ∧ ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) ↔ ( ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) ∧ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) )
2		elin	⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝐵 ∩ 𝐶 ) ↔ ( ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) )
3	2	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ( 𝐵 ∩ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐴 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) )
4		r19.26	⊢ ( ∀ 𝑥 ∈ 𝐴 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) )
5	3 4	bitri	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ( 𝐵 ∩ 𝐶 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) )
6	5	anbi2i	⊢ ( ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ( 𝐵 ∩ 𝐶 ) ) ↔ ( 𝑓 Fn 𝐴 ∧ ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) )
7		vex	⊢ 𝑓 ∈ V
8	7	elixp	⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) )
9	7	elixp	⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐶 ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) )
10	8 9	anbi12i	⊢ ( ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐶 ) ↔ ( ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) ∧ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) )
11	1 6 10	3bitr4i	⊢ ( ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ( 𝐵 ∩ 𝐶 ) ) ↔ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐶 ) )
12	7	elixp	⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ( 𝐵 ∩ 𝐶 ) ) )
13		elin	⊢ ( 𝑓 ∈ ( X 𝑥 ∈ 𝐴 𝐵 ∩ X 𝑥 ∈ 𝐴 𝐶 ) ↔ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐶 ) )
14	11 12 13	3bitr4i	⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) ↔ 𝑓 ∈ ( X 𝑥 ∈ 𝐴 𝐵 ∩ X 𝑥 ∈ 𝐴 𝐶 ) )
15	14	eqriv	⊢ X 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) = ( X 𝑥 ∈ 𝐴 𝐵 ∩ X 𝑥 ∈ 𝐴 𝐶 )