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

Metamath Proof Explorer

Theorem inxp

Description: Intersection of two Cartesian products. Exercise 9 of TakeutiZaring p. 25. (Contributed by NM, 3-Aug-1994) (Proof shortened by Andrew Salmon, 27-Aug-2011) Avoid ax-10 , ax-12 . (Revised by SN, 5-May-2025)

Ref Expression
Assertion inxp ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × 𝐷 ) ) = ( ( 𝐴 ∩ 𝐶 ) × ( 𝐵 ∩ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 relinxp ⊢ Rel ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × 𝐷 ) )
2 relxp ⊢ Rel ( ( 𝐴 ∩ 𝐶 ) × ( 𝐵 ∩ 𝐷 ) )
3 an4 ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ) )
4 opelxp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
5 opelxp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 × 𝐷 ) ↔ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) )
6 4 5 anbi12i ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 × 𝐷 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ) )
7 elin ⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) )
8 elin ⊢ ( 𝑦 ∈ ( 𝐵 ∩ 𝐷 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) )
9 7 8 anbi12i ⊢ ( ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∩ 𝐷 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ) )
10 3 6 9 3bitr4i ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 × 𝐷 ) ) ↔ ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∩ 𝐷 ) ) )
11 elin ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × 𝐷 ) ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 × 𝐷 ) ) )
12 opelxp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐴 ∩ 𝐶 ) × ( 𝐵 ∩ 𝐷 ) ) ↔ ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∩ 𝐷 ) ) )
13 10 11 12 3bitr4i ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × 𝐷 ) ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐴 ∩ 𝐶 ) × ( 𝐵 ∩ 𝐷 ) ) )
14 1 2 13 eqrelriiv ⊢ ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × 𝐷 ) ) = ( ( 𝐴 ∩ 𝐶 ) × ( 𝐵 ∩ 𝐷 ) )