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

Metamath Proof Explorer

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