Metamath Proof Explorer

Theorem difxp

Description: Difference of Cartesian products, expressed in terms of a union of Cartesian products of differences. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 26-Jun-2014) (Proof shortened by Wolf Lammen, 16-May-2025)

Ref Expression
Assertion difxp ( ( 𝐶 × 𝐷 ) ∖ ( 𝐴 × 𝐵 ) ) = ( ( ( 𝐶 ∖ 𝐴 ) × 𝐷 ) ∪ ( 𝐶 × ( 𝐷 ∖ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 difss ⊢ ( ( 𝐶 × 𝐷 ) ∖ ( 𝐴 × 𝐵 ) ) ⊆ ( 𝐶 × 𝐷 )
2 relxp ⊢ Rel ( 𝐶 × 𝐷 )
3 relss ⊢ ( ( ( 𝐶 × 𝐷 ) ∖ ( 𝐴 × 𝐵 ) ) ⊆ ( 𝐶 × 𝐷 ) → ( Rel ( 𝐶 × 𝐷 ) → Rel ( ( 𝐶 × 𝐷 ) ∖ ( 𝐴 × 𝐵 ) ) ) )
4 1 2 3 mp2 ⊢ Rel ( ( 𝐶 × 𝐷 ) ∖ ( 𝐴 × 𝐵 ) )
5 relxp ⊢ Rel ( ( 𝐶 ∖ 𝐴 ) × 𝐷 )
6 relxp ⊢ Rel ( 𝐶 × ( 𝐷 ∖ 𝐵 ) )
7 relun ⊢ ( Rel ( ( ( 𝐶 ∖ 𝐴 ) × 𝐷 ) ∪ ( 𝐶 × ( 𝐷 ∖ 𝐵 ) ) ) ↔ ( Rel ( ( 𝐶 ∖ 𝐴 ) × 𝐷 ) ∧ Rel ( 𝐶 × ( 𝐷 ∖ 𝐵 ) ) ) )
8 5 6 7 mpbir2an ⊢ Rel ( ( ( 𝐶 ∖ 𝐴 ) × 𝐷 ) ∪ ( 𝐶 × ( 𝐷 ∖ 𝐵 ) ) )
9 ianor ⊢ ( ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ↔ ( ¬ 𝑥 ∈ 𝐴 ∨ ¬ 𝑦 ∈ 𝐵 ) )
10 9 anbi2i ⊢ ( ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ↔ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ ( ¬ 𝑥 ∈ 𝐴 ∨ ¬ 𝑦 ∈ 𝐵 ) ) )
11 andi ⊢ ( ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ ( ¬ 𝑥 ∈ 𝐴 ∨ ¬ 𝑦 ∈ 𝐵 ) ) ↔ ( ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∨ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ 𝐵 ) ) )
12 10 11 bitri ⊢ ( ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ↔ ( ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∨ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ 𝐵 ) ) )
13 opelxp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 × 𝐷 ) ↔ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) )
14 opelxp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
15 14 notbii ⊢ ( ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ↔ ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
16 13 15 anbi12i ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 × 𝐷 ) ∧ ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ) ↔ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
17 opelxp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐶 ∖ 𝐴 ) × 𝐷 ) ↔ ( 𝑥 ∈ ( 𝐶 ∖ 𝐴 ) ∧ 𝑦 ∈ 𝐷 ) )
18 eldif ⊢ ( 𝑥 ∈ ( 𝐶 ∖ 𝐴 ) ↔ ( 𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐴 ) )
19 18 anbi1i ⊢ ( ( 𝑥 ∈ ( 𝐶 ∖ 𝐴 ) ∧ 𝑦 ∈ 𝐷 ) ↔ ( ( 𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐷 ) )
20 an32 ⊢ ( ( ( 𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐷 ) ↔ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑥 ∈ 𝐴 ) )
21 17 19 20 3bitri ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐶 ∖ 𝐴 ) × 𝐷 ) ↔ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑥 ∈ 𝐴 ) )
22 eldif ⊢ ( 𝑦 ∈ ( 𝐷 ∖ 𝐵 ) ↔ ( 𝑦 ∈ 𝐷 ∧ ¬ 𝑦 ∈ 𝐵 ) )
23 22 anbi2i ⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ ( 𝐷 ∖ 𝐵 ) ) ↔ ( 𝑥 ∈ 𝐶 ∧ ( 𝑦 ∈ 𝐷 ∧ ¬ 𝑦 ∈ 𝐵 ) ) )
24 opelxp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 × ( 𝐷 ∖ 𝐵 ) ) ↔ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ ( 𝐷 ∖ 𝐵 ) ) )
25 anass ⊢ ( ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐶 ∧ ( 𝑦 ∈ 𝐷 ∧ ¬ 𝑦 ∈ 𝐵 ) ) )
26 23 24 25 3bitr4i ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 × ( 𝐷 ∖ 𝐵 ) ) ↔ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ 𝐵 ) )
27 21 26 orbi12i ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐶 ∖ 𝐴 ) × 𝐷 ) ∨ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 × ( 𝐷 ∖ 𝐵 ) ) ) ↔ ( ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∨ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ 𝐵 ) ) )
28 12 16 27 3bitr4i ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 × 𝐷 ) ∧ ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐶 ∖ 𝐴 ) × 𝐷 ) ∨ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 × ( 𝐷 ∖ 𝐵 ) ) ) )
29 eldif ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐶 × 𝐷 ) ∖ ( 𝐴 × 𝐵 ) ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 × 𝐷 ) ∧ ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ) )
30 elun ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( ( 𝐶 ∖ 𝐴 ) × 𝐷 ) ∪ ( 𝐶 × ( 𝐷 ∖ 𝐵 ) ) ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐶 ∖ 𝐴 ) × 𝐷 ) ∨ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 × ( 𝐷 ∖ 𝐵 ) ) ) )
31 28 29 30 3bitr4i ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐶 × 𝐷 ) ∖ ( 𝐴 × 𝐵 ) ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( ( 𝐶 ∖ 𝐴 ) × 𝐷 ) ∪ ( 𝐶 × ( 𝐷 ∖ 𝐵 ) ) ) )
32 4 8 31 eqrelriiv ⊢ ( ( 𝐶 × 𝐷 ) ∖ ( 𝐴 × 𝐵 ) ) = ( ( ( 𝐶 ∖ 𝐴 ) × 𝐷 ) ∪ ( 𝐶 × ( 𝐷 ∖ 𝐵 ) ) )