difxp - Mathbox for Jeff Madsen

Mathbox for Jeff Madsen

< Previous Next >
Related theorems
Unicode version

Theorem difxp 15690

Description: Difference of Cartesian products, expressed in terms of a union of Cartesian products of differences.

**Assertion**
Ref	Expression
difxp

**Proof of Theorem difxp**
Step	Hyp	Ref	Expression
1		elxp6 5041	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
2	1	biimpri 169	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
3	2	anassrs 489	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
4	3	an1rs 547	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
5	4	ex 402	. . . . . . . . . . . . . . . 16 $/\$
6	5	con3d 111	. . . . . . . . . . . . . . 15 $/\$
7	6	expimpd 404	. . . . . . . . . . . . . 14 $/\$
8	7	ancomsd 485	. . . . . . . . . . . . 13 $/\$
9	8	anim2d 620	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
10		eldif 2609	. . . . . . . . . . . . . . 15 $/\$
11	10	biimpri 169	. . . . . . . . . . . . . 14 $/\$
12	11	anim1i 361	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
13	12	an1rs 547	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
14	9, 13	syl6 25	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
15	14	imdistani 491	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
16	15	anassrs 489	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
17		elxp6 5041	. . . . . . . . 9 $/\$ $/\$
18	16, 17	sylibr 217	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
19		elxp6 5041	. . . . . . . 8 $/\$ $/\$
20	18, 19	sylanb 498	. . . . . . 7 $/\$ $/\$
21	20	anassrs 489	. . . . . 6 $/\$ $/\$
22	21	orcd 294	. . . . 5 $/\$ $/\$ $\/$ $\/$
23		simpl 346	. . . . . . . . . . . . . . . 16 $/\$
24		eldif 2609	. . . . . . . . . . . . . . . . 17 $/\$
25	24	biimpri 169	. . . . . . . . . . . . . . . 16 $/\$
26	23, 25	anim12i 360	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
27	26	an42s 567	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
28	27	anim2i 362	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
29	28	anassrs 489	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30		elxp6 5041	. . . . . . . . . . . 12 $/\$ $/\$
31	29, 30	sylibr 217	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
32	31, 19	sylanb 498	. . . . . . . . . 10 $/\$ $/\$
33	32	anassrs 489	. . . . . . . . 9 $/\$ $/\$
34	33	adantllr 433	. . . . . . . 8 $/\$ $/\$ $/\$
35	34	orcd 294	. . . . . . 7 $/\$ $/\$ $/\$ $\/$
36	10, 24	anbi12i 540	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
37	36	biimpri 169	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
38	37	an42s 567	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
39	38	anim2i 362	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
40	39	anassrs 489	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
41		elxp6 5041	. . . . . . . . . . . 12 $/\$ $/\$
42	40, 41	sylibr 217	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
43	42, 19	sylanb 498	. . . . . . . . . 10 $/\$ $/\$
44	43	anassrs 489	. . . . . . . . 9 $/\$ $/\$
45	44	adantllr 433	. . . . . . . 8 $/\$ $/\$ $/\$
46	45	olcd 295	. . . . . . 7 $/\$ $/\$ $/\$ $\/$
47	35, 46	pm2.61dan 535	. . . . . 6 $/\$ $/\$ $\/$
48	47	olcd 295	. . . . 5 $/\$ $/\$ $\/$ $\/$
49	22, 48	pm2.61dan 535	. . . 4 $/\$ $\/$ $\/$
50		eldif 2609	. . . 4 $/\$
51		elun 2741	. . . . 5 $\/$
52		elun 2741	. . . . . 6 $\/$
53	52	orbi1i 276	. . . . 5 $\/$ $\/$ $\/$
54		orass 280	. . . . 5 $\/$ $\/$ $\/$ $\/$
55	51, 53, 54	3bitri 194	. . . 4 $\/$ $\/$
56	49, 50, 55	3imtr4i 236	. . 3
57		difss 2735	. . . . . . . . . 10
58		ssid 2634	. . . . . . . . . 10
59		xpss12 4089	. . . . . . . . . 10 $/\$
60	57, 58, 59	mp2an 761	. . . . . . . . 9
61	60	sseli 2617	. . . . . . . 8
62		xp1st 10155	. . . . . . . . 9
63		eldifn 2731	. . . . . . . . 9
64		xp1st 10155	. . . . . . . . . 10
65	64	con3i 114	. . . . . . . . 9
66	62, 63, 65	3syl 24	. . . . . . . 8
67	61, 66	jca 310	. . . . . . 7 $/\$
68		ssid 2634	. . . . . . . . . 10
69		difss 2735	. . . . . . . . . 10
70		xpss12 4089	. . . . . . . . . 10 $/\$
71	68, 69, 70	mp2an 761	. . . . . . . . 9
72	71	sseli 2617	. . . . . . . 8
73		xp2nd 10156	. . . . . . . . 9
74		eldifn 2731	. . . . . . . . 9
75		xp2nd 10156	. . . . . . . . . 10
76	75	con3i 114	. . . . . . . . 9
77	73, 74, 76	3syl 24	. . . . . . . 8
78	72, 77	jca 310	. . . . . . 7 $/\$
79	67, 78	jaoi 368	. . . . . 6 $\/$ $/\$
80	52, 79	sylbi 216	. . . . 5 $/\$
81		xpss12 4089	. . . . . . . 8 $/\$
82	57, 69, 81	mp2an 761	. . . . . . 7
83	82	sseli 2617	. . . . . 6
84		xp1st 10155	. . . . . . 7
85	84, 63, 65	3syl 24	. . . . . 6
86	83, 85	jca 310	. . . . 5 $/\$
87	80, 86	jaoi 368	. . . 4 $\/$ $/\$
88	87, 51, 50	3imtr4i 236	. . 3
89	56, 88	impbii 174	. 2
90	89	eqriv 1881	1

Colors of variables: wff set class

Syntax hints:

wn 2 $\/$ wo 239 $/\$ wa 240

wceq 1298

wcel 1300

cdif 2590

cun 2591

wss 2593

cop 3046

cxp 3984

cfv 3998

c1st 5018

c2nd 5019

This theorem is referenced by: txcld 15914

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1304 ax-gen 1305 ax-8 1306 ax-9 1307 ax-10 1308 ax-11 1309 ax-12 1310 ax-13 1311 ax-14 1312 ax-17 1317 ax-4 1319 ax-5o 1321 ax-6o 1324 ax-9o 1481 ax-10o 1500 ax-16 1580 ax-11o 1588 ax-ext 1865 ax-sep 3438 ax-nul 3445 ax-pow 3481 ax-pr 3524 ax-un 3790

This theorem depends on definitions: df-bi 164 df-or 241 df-an 242 df-ex 1327 df-sb 1536 df-eu 1775 df-mo 1776 df-clab 1872 df-cleq 1877 df-clel 1880 df-ne 2019 df-ral 2109 df-rex 2110 df-v 2294 df-dif 2597 df-un 2600 df-in 2603 df-ss 2605 df-nul 2876 df-pw 3035 df-sn 3049 df-pr 3050 df-op 3053 df-uni 3178 df-br 3339 df-opab 3396 df-id 3586 df-xp 4000 df-rel 4001 df-cnv 4002 df-co 4003 df-dm 4004 df-rn 4005 df-res 4006 df-ima 4007 df-fun 4008 df-fv 4014 df-1st 5020 df-2nd 5021