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	⊢ ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × 𝐷 ) ) = ( ( 𝐴 ∩ 𝐶 ) × ( 𝐵 ∩ 𝐷 ) )