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 |
19 20
|
bitri |
|- ( ( x e. ( C \ A ) /\ y e. D ) <-> ( ( x e. C /\ y e. D ) /\ -. x e. A ) ) |
22 |
17 21
|
bitri |
|- ( <. x , y >. e. ( ( C \ A ) X. D ) <-> ( ( x e. C /\ y e. D ) /\ -. x e. A ) ) |
23 |
|
eldif |
|- ( y e. ( D \ B ) <-> ( y e. D /\ -. y e. B ) ) |
24 |
23
|
anbi2i |
|- ( ( x e. C /\ y e. ( D \ B ) ) <-> ( x e. C /\ ( y e. D /\ -. y e. B ) ) ) |
25 |
|
opelxp |
|- ( <. x , y >. e. ( C X. ( D \ B ) ) <-> ( x e. C /\ y e. ( D \ B ) ) ) |
26 |
|
anass |
|- ( ( ( x e. C /\ y e. D ) /\ -. y e. B ) <-> ( x e. C /\ ( y e. D /\ -. y e. B ) ) ) |
27 |
24 25 26
|
3bitr4i |
|- ( <. x , y >. e. ( C X. ( D \ B ) ) <-> ( ( x e. C /\ y e. D ) /\ -. y e. B ) ) |
28 |
22 27
|
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 ) ) ) |
29 |
12 16 28
|
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 ) ) ) ) |
30 |
|
eldif |
|- ( <. x , y >. e. ( ( C X. D ) \ ( A X. B ) ) <-> ( <. x , y >. e. ( C X. D ) /\ -. <. x , y >. e. ( A X. B ) ) ) |
31 |
|
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 ) ) ) ) |
32 |
29 30 31
|
3bitr4i |
|- ( <. x , y >. e. ( ( C X. D ) \ ( A X. B ) ) <-> <. x , y >. e. ( ( ( C \ A ) X. D ) u. ( C X. ( D \ B ) ) ) ) |
33 |
4 8 32
|
eqrelriiv |
|- ( ( C X. D ) \ ( A X. B ) ) = ( ( ( C \ A ) X. D ) u. ( C X. ( D \ B ) ) ) |