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

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 
|- ( ( C X. D ) \ ( A X. B ) ) = ( ( ( C \ A ) X. D ) u. ( C X. ( D \ B ) ) )

Proof

Step Hyp Ref Expression
1 difss 
 |-  ( ( C X. D ) \ ( A X. B ) ) C_ ( C X. D )
2 relxp 
 |-  Rel ( C X. D )
3 relss 
 |-  ( ( ( C X. D ) \ ( A X. B ) ) C_ ( C X. D ) -> ( Rel ( C X. D ) -> Rel ( ( C X. D ) \ ( A X. B ) ) ) )
4 1 2 3 mp2 
 |-  Rel ( ( C X. D ) \ ( A X. B ) )
5 relxp 
 |-  Rel ( ( C \ A ) X. D )
6 relxp 
 |-  Rel ( C X. ( D \ B ) )
7 relun 
 |-  ( Rel ( ( ( C \ A ) X. D ) u. ( C X. ( D \ B ) ) ) <-> ( Rel ( ( C \ A ) X. D ) /\ Rel ( C X. ( D \ B ) ) ) )
8 5 6 7 mpbir2an 
 |-  Rel ( ( ( C \ A ) X. D ) u. ( C X. ( D \ B ) ) )
9 ianor 
 |-  ( -. ( x e. A /\ y e. B ) <-> ( -. x e. A \/ -. y e. B ) )
10 9 anbi2i 
 |-  ( ( ( x e. C /\ y e. D ) /\ -. ( x e. A /\ y e. B ) ) <-> ( ( x e. C /\ y e. D ) /\ ( -. x e. A \/ -. y e. B ) ) )
11 andi 
 |-  ( ( ( x e. C /\ y e. D ) /\ ( -. x e. A \/ -. y e. B ) ) <-> ( ( ( x e. C /\ y e. D ) /\ -. x e. A ) \/ ( ( x e. C /\ y e. D ) /\ -. y e. B ) ) )
12 10 11 bitri 
 |-  ( ( ( x e. C /\ y e. D ) /\ -. ( x e. A /\ y e. B ) ) <-> ( ( ( x e. C /\ y e. D ) /\ -. x e. A ) \/ ( ( x e. C /\ y e. D ) /\ -. y e. B ) ) )
13 opelxp 
 |-  ( <. x , y >. e. ( C X. D ) <-> ( x e. C /\ y e. D ) )
14 opelxp 
 |-  ( <. x , y >. e. ( A X. B ) <-> ( x e. A /\ y e. B ) )
15 14 notbii 
 |-  ( -. <. x , y >. e. ( A X. B ) <-> -. ( x e. A /\ y e. B ) )
16 13 15 anbi12i 
 |-  ( ( <. x , y >. e. ( C X. D ) /\ -. <. x , y >. e. ( A X. B ) ) <-> ( ( x e. C /\ y e. D ) /\ -. ( x e. A /\ y e. B ) ) )
17 opelxp 
 |-  ( <. x , y >. e. ( ( C \ A ) X. D ) <-> ( x e. ( C \ A ) /\ y e. D ) )
18 eldif 
 |-  ( x e. ( C \ A ) <-> ( x e. C /\ -. x e. A ) )
19 18 anbi1i 
 |-  ( ( x e. ( C \ A ) /\ y e. D ) <-> ( ( x e. C /\ -. x e. A ) /\ y e. D ) )
20 an32 
 |-  ( ( ( x e. C /\ -. x e. A ) /\ y e. D ) <-> ( ( x e. C /\ y e. D ) /\ -. x e. A ) )
21 17 19 20 3bitri 
 |-  ( <. x , y >. e. ( ( C \ A ) X. D ) <-> ( ( x e. C /\ y e. D ) /\ -. x e. A ) )
22 eldif 
 |-  ( y e. ( D \ B ) <-> ( y e. D /\ -. y e. B ) )
23 22 anbi2i 
 |-  ( ( x e. C /\ y e. ( D \ B ) ) <-> ( x e. C /\ ( y e. D /\ -. y e. B ) ) )
24 opelxp 
 |-  ( <. x , y >. e. ( C X. ( D \ B ) ) <-> ( x e. C /\ y e. ( D \ B ) ) )
25 anass 
 |-  ( ( ( x e. C /\ y e. D ) /\ -. y e. B ) <-> ( x e. C /\ ( y e. D /\ -. y e. B ) ) )
26 23 24 25 3bitr4i 
 |-  ( <. x , y >. e. ( C X. ( D \ B ) ) <-> ( ( x e. C /\ y e. D ) /\ -. y e. B ) )
27 21 26 orbi12i 
 |-  ( ( <. x , y >. e. ( ( C \ A ) X. D ) \/ <. x , y >. e. ( C X. ( D \ B ) ) ) <-> ( ( ( x e. C /\ y e. D ) /\ -. x e. A ) \/ ( ( x e. C /\ y e. D ) /\ -. y e. B ) ) )
28 12 16 27 3bitr4i 
 |-  ( ( <. x , y >. e. ( C X. D ) /\ -. <. x , y >. e. ( A X. B ) ) <-> ( <. x , y >. e. ( ( C \ A ) X. D ) \/ <. x , y >. e. ( C X. ( D \ B ) ) ) )
29 eldif 
 |-  ( <. x , y >. e. ( ( C X. D ) \ ( A X. B ) ) <-> ( <. x , y >. e. ( C X. D ) /\ -. <. x , y >. e. ( A X. B ) ) )
30 elun 
 |-  ( <. x , y >. e. ( ( ( C \ A ) X. D ) u. ( C X. ( D \ B ) ) ) <-> ( <. x , y >. e. ( ( C \ A ) X. D ) \/ <. x , y >. e. ( C X. ( D \ B ) ) ) )
31 28 29 30 3bitr4i 
 |-  ( <. x , y >. e. ( ( C X. D ) \ ( A X. B ) ) <-> <. x , y >. e. ( ( ( C \ A ) X. D ) u. ( C X. ( D \ B ) ) ) )
32 4 8 31 eqrelriiv 
 |-  ( ( C X. D ) \ ( A X. B ) ) = ( ( ( C \ A ) X. D ) u. ( C X. ( D \ B ) ) )