imadifxp - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > imadifxp		Structured version Visualization version Unicode version

Theorem imadifxp 29414

Description: Image of the difference with a Cartesian product. (Contributed by Thierry Arnoux, 13-Dec-2017.)

**Assertion**
Ref	Expression
imadifxp	$\$ $\$

**Proof of Theorem imadifxp**
Step	Hyp	Ref	Expression
1		ima0 5481	. . . 4 $\$
2		imaeq2 5462	. . . 4 $\$ $\$
3		imaeq2 5462	. . . . . . 7
4		ima0 5481	. . . . . . 7
5	3, 4	syl6eq 2672	. . . . . 6
6	5	difeq1d 3727	. . . . 5 $\$ $\$
7		0dif 3977	. . . . 5 $\$
8	6, 7	syl6eq 2672	. . . 4 $\$
9	1, 2, 8	3eqtr4a 2682	. . 3 $\$ $\$
10	9	adantl 482	. 2 $/\$ $\$ $\$
11		inundif 4046	. . . . . . . . 9 $\$
12	11	imaeq1i 5463	. . . . . . . 8 $\$
13		imaundir 5546	. . . . . . . 8 $\$ $\$
14	12, 13	eqtr3i 2646	. . . . . . 7 $\$
15	14	difeq1i 3724	. . . . . 6 $\$ $\$ $\$
16		difundir 3880	. . . . . 6 $\$ $\$ $\$ $\$ $\$
17	15, 16	eqtri 2644	. . . . 5 $\$ $\$ $\$ $\$
18		inss2 3834	. . . . . . . . 9
19		imass1 5500	. . . . . . . . 9
20		ssdif 3745	. . . . . . . . 9 $\$ $\$
21	18, 19, 20	mp2b 10	. . . . . . . 8 $\$ $\$
22		xpima 5576	. . . . . . . . . . 11
23		incom 3805	. . . . . . . . . . . . . . 15
24		df-ss 3588	. . . . . . . . . . . . . . . 16
25	24	biimpi 206	. . . . . . . . . . . . . . 15
26	23, 25	syl5eqr 2670	. . . . . . . . . . . . . 14
27	26	adantl 482	. . . . . . . . . . . . 13 $/\$
28		simpl 473	. . . . . . . . . . . . 13 $/\$
29	27, 28	eqnetrd 2861	. . . . . . . . . . . 12 $/\$
30		df-ne 2795	. . . . . . . . . . . . 13
31	30	biimpi 206	. . . . . . . . . . . 12
32		iffalse 4095	. . . . . . . . . . . 12
33	29, 31, 32	3syl 18	. . . . . . . . . . 11 $/\$
34	22, 33	syl5eq 2668	. . . . . . . . . 10 $/\$
35	34	difeq1d 3727	. . . . . . . . 9 $/\$ $\$ $\$
36		difid 3948	. . . . . . . . 9 $\$
37	35, 36	syl6eq 2672	. . . . . . . 8 $/\$ $\$
38	21, 37	syl5sseq 3653	. . . . . . 7 $/\$ $\$
39		ss0 3974	. . . . . . 7 $\$ $\$
40	38, 39	syl 17	. . . . . 6 $/\$ $\$
41		df-ima 5127	. . . . . . . . . . 11 $\$ $\$
42		df-res 5126	. . . . . . . . . . . 12 $\$ $\$
43	42	rneqi 5352	. . . . . . . . . . 11 $\$ $\$
44	41, 43	eqtri 2644	. . . . . . . . . 10 $\$ $\$
45	44	ineq1i 3810	. . . . . . . . 9 $\$ $\$
46		xpss1 5228	. . . . . . . . . . . 12
47		sslin 3839	. . . . . . . . . . . 12 $\$ $\$
48		rnss 5354	. . . . . . . . . . . 12 $\$ $\$ $\$ $\$
49	46, 47, 48	3syl 18	. . . . . . . . . . 11 $\$ $\$
50	49	adantl 482	. . . . . . . . . 10 $/\$ $\$ $\$
51		ssn0 3976	. . . . . . . . . . . 12 $/\$
52	51	ancoms 469	. . . . . . . . . . 11 $/\$
53		inss1 3833	. . . . . . . . . . . . . . . 16
54		ssdif 3745	. . . . . . . . . . . . . . . 16 $\$ $\$
55	53, 54	ax-mp 5	. . . . . . . . . . . . . . 15 $\$ $\$
56		incom 3805	. . . . . . . . . . . . . . . 16 $\$ $\$
57		indif2 3870	. . . . . . . . . . . . . . . 16 $\$ $\$
58	56, 57	eqtr3i 2646	. . . . . . . . . . . . . . 15 $\$ $\$
59		difxp2 5560	. . . . . . . . . . . . . . 15 $\$ $\$
60	55, 58, 59	3sstr4i 3644	. . . . . . . . . . . . . 14 $\$ $\$
61		rnss 5354	. . . . . . . . . . . . . 14 $\$ $\$ $\$ $\$
62	60, 61	mp1i 13	. . . . . . . . . . . . 13 $\$ $\$
63		rnxp 5564	. . . . . . . . . . . . 13 $\$ $\$
64	62, 63	sseqtrd 3641	. . . . . . . . . . . 12 $\$ $\$
65		disj2 4024	. . . . . . . . . . . 12 $\$ $\$ $\$
66	64, 65	sylibr 224	. . . . . . . . . . 11 $\$
67	52, 66	syl 17	. . . . . . . . . 10 $/\$ $\$
68		ssdisj 4026	. . . . . . . . . 10 $\$ $\$ $/\$ $\$ $\$
69	50, 67, 68	syl2anc 693	. . . . . . . . 9 $/\$ $\$
70	45, 69	syl5eq 2668	. . . . . . . 8 $/\$ $\$
71		disj3 4021	. . . . . . . 8 $\$ $\$ $\$ $\$
72	70, 71	sylib 208	. . . . . . 7 $/\$ $\$ $\$ $\$
73	72	eqcomd 2628	. . . . . 6 $/\$ $\$ $\$ $\$
74	40, 73	uneq12d 3768	. . . . 5 $/\$ $\$ $\$ $\$ $\$
75	17, 74	syl5eq 2668	. . . 4 $/\$ $\$ $\$
76		uncom 3757	. . . . 5 $\$ $\$
77		un0 3967	. . . . 5 $\$ $\$
78	76, 77	eqtr2i 2645	. . . 4 $\$ $\$
79	75, 78	syl6reqr 2675	. . 3 $/\$ $\$ $\$
80	79	ancoms 469	. 2 $/\$ $\$ $\$
81	10, 80	pm2.61dane 2881	1 $\$ $\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 384

wceq 1483

wne 2794

cvv 3200 $\$ cdif 3571

cun 3572

cin 3573

wss 3574

c0 3915

cif 4086

cxp 5112

crn 5115

cres 5116

cima 5117

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pr 4906

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-br 4654 df-opab 4713 df-xp 5120 df-rel 5121 df-cnv 5122 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127

This theorem is referenced by: (None)

W3C validator