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)

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

Proof

Step	Hyp	Ref	Expression
1		inopab	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ) }
2		an4	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ) )
3		elin	⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) )
4		elin	⊢ ( 𝑦 ∈ ( 𝐵 ∩ 𝐷 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) )
5	3 4	anbi12i	⊢ ( ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∩ 𝐷 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ) )
6	2 5	bitr4i	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ) ↔ ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∩ 𝐷 ) ) )
7	6	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∩ 𝐷 ) ) }
8	1 7	eqtri	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∩ 𝐷 ) ) }
9		df-xp	⊢ ( 𝐴 × 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) }
10		df-xp	⊢ ( 𝐶 × 𝐷 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) }
11	9 10	ineq12i	⊢ ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × 𝐷 ) ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) } )
12		df-xp	⊢ ( ( 𝐴 ∩ 𝐶 ) × ( 𝐵 ∩ 𝐷 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∩ 𝐷 ) ) }
13	8 11 12	3eqtr4i	⊢ ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × 𝐷 ) ) = ( ( 𝐴 ∩ 𝐶 ) × ( 𝐵 ∩ 𝐷 ) )