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)

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 19 20 bitri ( ( 𝑥 ∈ ( 𝐶𝐴 ) ∧ 𝑦𝐷 ) ↔ ( ( 𝑥𝐶𝑦𝐷 ) ∧ ¬ 𝑥𝐴 ) )
22 17 21 bitri ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐶𝐴 ) × 𝐷 ) ↔ ( ( 𝑥𝐶𝑦𝐷 ) ∧ ¬ 𝑥𝐴 ) )
23 eldif ( 𝑦 ∈ ( 𝐷𝐵 ) ↔ ( 𝑦𝐷 ∧ ¬ 𝑦𝐵 ) )
24 23 anbi2i ( ( 𝑥𝐶𝑦 ∈ ( 𝐷𝐵 ) ) ↔ ( 𝑥𝐶 ∧ ( 𝑦𝐷 ∧ ¬ 𝑦𝐵 ) ) )
25 opelxp ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 × ( 𝐷𝐵 ) ) ↔ ( 𝑥𝐶𝑦 ∈ ( 𝐷𝐵 ) ) )
26 anass ( ( ( 𝑥𝐶𝑦𝐷 ) ∧ ¬ 𝑦𝐵 ) ↔ ( 𝑥𝐶 ∧ ( 𝑦𝐷 ∧ ¬ 𝑦𝐵 ) ) )
27 24 25 26 3bitr4i ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 × ( 𝐷𝐵 ) ) ↔ ( ( 𝑥𝐶𝑦𝐷 ) ∧ ¬ 𝑦𝐵 ) )
28 22 27 orbi12i ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐶𝐴 ) × 𝐷 ) ∨ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 × ( 𝐷𝐵 ) ) ) ↔ ( ( ( 𝑥𝐶𝑦𝐷 ) ∧ ¬ 𝑥𝐴 ) ∨ ( ( 𝑥𝐶𝑦𝐷 ) ∧ ¬ 𝑦𝐵 ) ) )
29 12 16 28 3bitr4i ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 × 𝐷 ) ∧ ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐶𝐴 ) × 𝐷 ) ∨ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 × ( 𝐷𝐵 ) ) ) )
30 eldif ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐶 × 𝐷 ) ∖ ( 𝐴 × 𝐵 ) ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 × 𝐷 ) ∧ ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ) )
31 elun ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( ( 𝐶𝐴 ) × 𝐷 ) ∪ ( 𝐶 × ( 𝐷𝐵 ) ) ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐶𝐴 ) × 𝐷 ) ∨ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 × ( 𝐷𝐵 ) ) ) )
32 29 30 31 3bitr4i ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐶 × 𝐷 ) ∖ ( 𝐴 × 𝐵 ) ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( ( 𝐶𝐴 ) × 𝐷 ) ∪ ( 𝐶 × ( 𝐷𝐵 ) ) ) )
33 4 8 32 eqrelriiv ( ( 𝐶 × 𝐷 ) ∖ ( 𝐴 × 𝐵 ) ) = ( ( ( 𝐶𝐴 ) × 𝐷 ) ∪ ( 𝐶 × ( 𝐷𝐵 ) ) )