Theorem incexclem 13648

Description: Lemma for incexc 13649. (Contributed by Mario Carneiro, 7-Aug-2017.)

Assertion

Ref	Expression
incexclem

Distinct variable groups:   ,   ,

Proof of Theorem incexclem

Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		unieq 4257	. . . . . . . . . . 11
2		uni0 4276	. . . . . . . . . . 11
3	1, 2	syl6eq 2514	. . . . . . . . . 10
4	3	ineq2d 3699	. . . . . . . . 9
5		in0 3811	. . . . . . . . 9
6	4, 5	syl6eq 2514	. . . . . . . 8
7	6	fveq2d 5875	. . . . . . 7
8		hash0 12437	. . . . . . 7
9	7, 8	syl6eq 2514	. . . . . 6
10	9	oveq2d 6312	. . . . 5
11		pweq 4015	. . . . . . 7
12		pw0 4177	. . . . . . 7
13	11, 12	syl6eq 2514	. . . . . 6
14	13	sumeq1d 13523	. . . . 5
15	10, 14	eqeq12d 2479	. . . 4
16	15	ralbidv 2896	. . 3
17		unieq 4257	. . . . . . . 8
18	17	ineq2d 3699	. . . . . . 7
19	18	fveq2d 5875	. . . . . 6
20	19	oveq2d 6312	. . . . 5
21		pweq 4015	. . . . . 6
22	21	sumeq1d 13523	. . . . 5
23	20, 22	eqeq12d 2479	. . . 4
24	23	ralbidv 2896	. . 3
25		unieq 4257	. . . . . . . . 9
26		uniun 4268	. . . . . . . . . 10
27		vex 3112	. . . . . . . . . . . 12
28	27	unisn 4264	. . . . . . . . . . 11
29	28	uneq2i 3654	. . . . . . . . . 10
30	26, 29	eqtri 2486	. . . . . . . . 9
31	25, 30	syl6eq 2514	. . . . . . . 8
32	31	ineq2d 3699	. . . . . . 7
33	32	fveq2d 5875	. . . . . 6
34	33	oveq2d 6312	. . . . 5
35		pweq 4015	. . . . . 6
36	35	sumeq1d 13523	. . . . 5
37	34, 36	eqeq12d 2479	. . . 4
38	37	ralbidv 2896	. . 3
39		unieq 4257	. . . . . . . 8
40	39	ineq2d 3699	. . . . . . 7
41	40	fveq2d 5875	. . . . . 6
42	41	oveq2d 6312	. . . . 5
43		pweq 4015	. . . . . 6
44	43	sumeq1d 13523	. . . . 5
45	42, 44	eqeq12d 2479	. . . 4
46	45	ralbidv 2896	. . 3
47		hashcl 12428	. . . . . . 7
48	47	nn0cnd 10879	. . . . . 6
49	48	mulid2d 9635	. . . . 5
50		0ex 4582	. . . . . 6
51	49, 48	eqeltrd 2545	. . . . . 6
52		fveq2 5871	. . . . . . . . . . 11
53	52, 8	syl6eq 2514	. . . . . . . . . 10
54	53	oveq2d 6312	. . . . . . . . 9
55		neg1cn 10664	. . . . . . . . . 10
56		exp0 12170	. . . . . . . . . 10
57	55, 56	ax-mp 5	. . . . . . . . 9
58	54, 57	syl6eq 2514	. . . . . . . 8
59		rint0 4327	. . . . . . . . 9
60	59	fveq2d 5875	. . . . . . . 8
61	58, 60	oveq12d 6314	. . . . . . 7
62	61	sumsn 13563	. . . . . 6
63	50, 51, 62	sylancr 663	. . . . 5
64	48	subid1d 9943	. . . . 5
65	49, 63, 64	3eqtr4rd 2509	. . . 4
66	65	rgen 2817	. . 3
67		fveq2 5871	. . . . . . . . . . . 12
68		ineq1 3692	. . . . . . . . . . . . 13
69	68	fveq2d 5875	. . . . . . . . . . . 12
70	67, 69	oveq12d 6314	. . . . . . . . . . 11
71		simpl 457	. . . . . . . . . . . . . . 15
72	71	ineq1d 3698	. . . . . . . . . . . . . 14
73	72	fveq2d 5875	. . . . . . . . . . . . 13
74	73	oveq2d 6312	. . . . . . . . . . . 12
75	74	sumeq2dv 13525	. . . . . . . . . . 11
76	70, 75	eqeq12d 2479	. . . . . . . . . 10
77	76	rspcva 3208	. . . . . . . . 9
78	77	adantll 713	. . . . . . . 8
79		simpr 461	. . . . . . . . . 10
80		inss1 3717	. . . . . . . . . 10
81		ssfi 7760	. . . . . . . . . 10
82	79, 80, 81	sylancl 662	. . . . . . . . 9
83		fveq2 5871	. . . . . . . . . . . 12
84		ineq1 3692	. . . . . . . . . . . . . 14
85		in32 3709	. . . . . . . . . . . . . . 15
86		inass 3707	. . . . . . . . . . . . . . 15
87	85, 86	eqtri 2486	. . . . . . . . . . . . . 14
88	84, 87	syl6eq 2514	. . . . . . . . . . . . 13
89	88	fveq2d 5875	. . . . . . . . . . . 12
90	83, 89	oveq12d 6314	. . . . . . . . . . 11
91		ineq1 3692	. . . . . . . . . . . . . . 15
92		in32 3709	. . . . . . . . . . . . . . . 16
93		inass 3707	. . . . . . . . . . . . . . . 16
94	92, 93	eqtri 2486	. . . . . . . . . . . . . . 15
95	91, 94	syl6eq 2514	. . . . . . . . . . . . . 14
96	95	fveq2d 5875	. . . . . . . . . . . . 13
97	96	oveq2d 6312	. . . . . . . . . . . 12
98	97	sumeq2sdv 13526	. . . . . . . . . . 11
99	90, 98	eqeq12d 2479	. . . . . . . . . 10
100	99	rspcva 3208	. . . . . . . . 9
101	82, 100	sylan 471	. . . . . . . 8
102	78, 101	oveq12d 6314	. . . . . . 7
103		inss1 3717	. . . . . . . . . . . . . 14
104		ssfi 7760	. . . . . . . . . . . . . 14
105	79, 103, 104	sylancl 662	. . . . . . . . . . . . 13
106		hashun3 12452	. . . . . . . . . . . . 13
107	105, 82, 106	syl2anc 661	. . . . . . . . . . . 12
108		indi 3743	. . . . . . . . . . . . 13
109	108	fveq2i 5874	. . . . . . . . . . . 12
110		inindi 3714	. . . . . . . . . . . . . 14
111	110	fveq2i 5874	. . . . . . . . . . . . 13
112	111	oveq2i 6307	. . . . . . . . . . . 12
113	107, 109, 112	3eqtr4g 2523	. . . . . . . . . . 11
114		hashcl 12428	. . . . . . . . . . . . . 14
115	105, 114	syl 16	. . . . . . . . . . . . 13
116	115	nn0cnd 10879	. . . . . . . . . . . 12
117		hashcl 12428	. . . . . . . . . . . . . 14
118	82, 117	syl 16	. . . . . . . . . . . . 13
119	118	nn0cnd 10879	. . . . . . . . . . . 12
120		inss1 3717	. . . . . . . . . . . . . . 15
121		ssfi 7760	. . . . . . . . . . . . . . 15
122	79, 120, 121	sylancl 662	. . . . . . . . . . . . . 14
123		hashcl 12428	. . . . . . . . . . . . . 14
124	122, 123	syl 16	. . . . . . . . . . . . 13
125	124	nn0cnd 10879	. . . . . . . . . . . 12
126	116, 119, 125	addsubassd 9974	. . . . . . . . . . 11
127	113, 126	eqtrd 2498	. . . . . . . . . 10
128	127	oveq2d 6312	. . . . . . . . 9
129		hashcl 12428	. . . . . . . . . . . 12
130	129	adantl 466	. . . . . . . . . . 11
131	130	nn0cnd 10879	. . . . . . . . . 10
132	119, 125	subcld 9954	. . . . . . . . . 10
133	131, 116, 132	subsub4d 9985	. . . . . . . . 9
134	128, 133	eqtr4d 2501	. . . . . . . 8
135	134	adantr 465	. . . . . . 7
136		disjdif 3900	. . . . . . . . . . 11
137	136	a1i 11	. . . . . . . . . 10
138		ssun1 3666	. . . . . . . . . . . . . 14
139		sspwb 4701	. . . . . . . . . . . . . 14
140	138, 139	mpbi 208	. . . . . . . . . . . . 13
141		undif 3908	. . . . . . . . . . . . 13
142	140, 141	mpbi 208	. . . . . . . . . . . 12
143	142	eqcomi 2470	. . . . . . . . . . 11
144	143	a1i 11	. . . . . . . . . 10
145		simpll 753	. . . . . . . . . . . 12
146		snfi 7616	. . . . . . . . . . . 12
147		unfi 7807	. . . . . . . . . . . 12
148	145, 146, 147	sylancl 662	. . . . . . . . . . 11
149		pwfi 7835	. . . . . . . . . . 11
150	148, 149	sylib 196	. . . . . . . . . 10
151	55	a1i 11	. . . . . . . . . . . 12
152		elpwi 4021	. . . . . . . . . . . . . 14
153		ssfi 7760	. . . . . . . . . . . . . 14
154	148, 152, 153	syl2an 477	. . . . . . . . . . . . 13
155		hashcl 12428	. . . . . . . . . . . . 13
156	154, 155	syl 16	. . . . . . . . . . . 12
157	151, 156	expcld 12310	. . . . . . . . . . 11
158		simplr 755	. . . . . . . . . . . . . 14
159		inss1 3717	. . . . . . . . . . . . . 14
160		ssfi 7760	. . . . . . . . . . . . . 14
161	158, 159, 160	sylancl 662	. . . . . . . . . . . . 13
162		hashcl 12428	. . . . . . . . . . . . 13
163	161, 162	syl 16	. . . . . . . . . . . 12
164	163	nn0cnd 10879	. . . . . . . . . . 11
165	157, 164	mulcld 9637	. . . . . . . . . 10
166	137, 144, 150, 165	fsumsplit 13562	. . . . . . . . 9
167		fveq2 5871	. . . . . . . . . . . . . 14
168	167	oveq2d 6312	. . . . . . . . . . . . 13
169		inteq 4289	. . . . . . . . . . . . . . . 16
170	27	intunsn 4326	. . . . . . . . . . . . . . . 16
171	169, 170	syl6eq 2514	. . . . . . . . . . . . . . 15
172	171	ineq2d 3699	. . . . . . . . . . . . . 14
173	172	fveq2d 5875	. . . . . . . . . . . . 13
174	168, 173	oveq12d 6314	. . . . . . . . . . . 12
175		pwfi 7835	. . . . . . . . . . . . 13
176	145, 175	sylib 196	. . . . . . . . . . . 12
177		eqid 2457	. . . . . . . . . . . . 13
178		elpwi 4021	. . . . . . . . . . . . . . . . 17
179	178	adantl 466	. . . . . . . . . . . . . . . 16
180		unss1 3672	. . . . . . . . . . . . . . . 16
181	179, 180	syl 16	. . . . . . . . . . . . . . 15
182		vex 3112	. . . . . . . . . . . . . . . . 17
183		snex 4693	. . . . . . . . . . . . . . . . 17
184	182, 183	unex 6598	. . . . . . . . . . . . . . . 16
185	184	elpw 4018	. . . . . . . . . . . . . . 15
186	181, 185	sylibr 212	. . . . . . . . . . . . . 14
187		simpllr 760	. . . . . . . . . . . . . . 15
188		elpwi 4021	. . . . . . . . . . . . . . . 16
189		ssun2 3667	. . . . . . . . . . . . . . . . . . 19
190	27	snss 4154	. . . . . . . . . . . . . . . . . . 19
191	189, 190	mpbir 209	. . . . . . . . . . . . . . . . . 18
192	191	a1i 11	. . . . . . . . . . . . . . . . 17
193		ssel 3497	. . . . . . . . . . . . . . . . 17
194	192, 193	syl5com 30	. . . . . . . . . . . . . . . 16
195	188, 194	syl5 32	. . . . . . . . . . . . . . 15
196	187, 195	mtod 177	. . . . . . . . . . . . . 14
197	186, 196	eldifd 3486	. . . . . . . . . . . . 13
198		eldifi 3625	. . . . . . . . . . . . . . . . . 18
199	198	adantl 466	. . . . . . . . . . . . . . . . 17
200	199	elpwid 4022	. . . . . . . . . . . . . . . 16
201		uncom 3647	. . . . . . . . . . . . . . . 16
202	200, 201	syl6sseq 3549	. . . . . . . . . . . . . . 15
203		ssundif 3911	. . . . . . . . . . . . . . 15
204	202, 203	sylib 196	. . . . . . . . . . . . . 14
205		vex 3112	. . . . . . . . . . . . . . 15
206	205	elpw2 4616	. . . . . . . . . . . . . 14
207	204, 206	sylibr 212	. . . . . . . . . . . . 13
208		elpwunsn 4070	. . . . . . . . . . . . . . . . . . 19
209	208	ad2antll 728	. . . . . . . . . . . . . . . . . 18
210	209	snssd 4175	. . . . . . . . . . . . . . . . 17
211		ssequn2 3676	. . . . . . . . . . . . . . . . 17
212	210, 211	sylib 196	. . . . . . . . . . . . . . . 16
213	212	eqcomd 2465	. . . . . . . . . . . . . . 15
214		uneq1 3650	. . . . . . . . . . . . . . . . 17
215		undif1 3903	. . . . . . . . . . . . . . . . 17
216	214, 215	syl6eq 2514	. . . . . . . . . . . . . . . 16
217	216	eqeq2d 2471	. . . . . . . . . . . . . . 15
218	213, 217	syl5ibrcom 222	. . . . . . . . . . . . . 14
219	178	ad2antrl 727	. . . . . . . . . . . . . . . . . 18
220		simpllr 760	. . . . . . . . . . . . . . . . . 18
221	219, 220	ssneldd 3506	. . . . . . . . . . . . . . . . 17
222		difsnb 4172	. . . . . . . . . . . . . . . . 17
223	221, 222	sylib 196	. . . . . . . . . . . . . . . 16
224	223	eqcomd 2465	. . . . . . . . . . . . . . 15
225		difeq1 3614	. . . . . . . . . . . . . . . . 17
226		difun2 3907	. . . . . . . . . . . . . . . . 17
227	225, 226	syl6eq 2514	. . . . . . . . . . . . . . . 16
228	227	eqeq2d 2471	. . . . . . . . . . . . . . 15
229	224, 228	syl5ibrcom 222	. . . . . . . . . . . . . 14
230	218, 229	impbid 191	. . . . . . . . . . . . 13
231	177, 197, 207, 230	f1o2d 6527	. . . . . . . . . . . 12
232		uneq1 3650	. . . . . . . . . . . . . 14
233		vex 3112	. . . . . . . . . . . . . . 15
234	233, 183	unex 6598	. . . . . . . . . . . . . 14
235	232, 177, 234	fvmpt 5956	. . . . . . . . . . . . 13
236	235	adantl 466	. . . . . . . . . . . 12
237	198, 165	sylan2 474	. . . . . . . . . . . 12
238	174, 176, 231, 236, 237	fsumf1o 13545	. . . . . . . . . . 11
239		uneq1 3650	. . . . . . . . . . . . . . . 16
240	239	fveq2d 5875	. . . . . . . . . . . . . . 15
241	240	oveq2d 6312	. . . . . . . . . . . . . 14
242		inteq 4289	. . . . . . . . . . . . . . . . 17
243	242	ineq1d 3698	. . . . . . . . . . . . . . . 16
244	243	ineq2d 3699	. . . . . . . . . . . . . . 15
245	244	fveq2d 5875	. . . . . . . . . . . . . 14
246	241, 245	oveq12d 6314	. . . . . . . . . . . . 13
247	246	cbvsumv 13518	. . . . . . . . . . . 12
248		elpwi 4021	. . . . . . . . . . . . . . . . . . . 20
249		ssfi 7760	. . . . . . . . . . . . . . . . . . . 20
250	145, 248, 249	syl2an 477	. . . . . . . . . . . . . . . . . . 19
251	248	adantl 466	. . . . . . . . . . . . . . . . . . . 20
252		simpllr 760	. . . . . . . . . . . . . . . . . . . 20
253	251, 252	ssneldd 3506	. . . . . . . . . . . . . . . . . . 19
254		hashunsng 12459	. . . . . . . . . . . . . . . . . . . 20
255	27, 254	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
256	250, 253, 255	syl2anc 661	. . . . . . . . . . . . . . . . . 18
257	256	oveq2d 6312	. . . . . . . . . . . . . . . . 17
258	55	a1i 11	. . . . . . . . . . . . . . . . . 18
259	250, 155	syl 16	. . . . . . . . . . . . . . . . . 18
260	258, 259	expp1d 12311	. . . . . . . . . . . . . . . . 17
261	257, 260	eqtrd 2498	. . . . . . . . . . . . . . . 16
262	140	sseli 3499	. . . . . . . . . . . . . . . . . 18
263	262, 157	sylan2 474	. . . . . . . . . . . . . . . . 17
264	258, 263	mulcomd 9638	. . . . . . . . . . . . . . . 16
265	263	mulm1d 10033	. . . . . . . . . . . . . . . 16
266	261, 264, 265	3eqtr2d 2504	. . . . . . . . . . . . . . 15
267	266	oveq1d 6311	. . . . . . . . . . . . . 14
268		inss1 3717	. . . . . . . . . . . . . . . . . . 19
269		ssfi 7760	. . . . . . . . . . . . . . . . . . 19
270	158, 268, 269	sylancl 662	. . . . . . . . . . . . . . . . . 18
271		hashcl 12428	. . . . . . . . . . . . . . . . . 18
272	270, 271	syl 16	. . . . . . . . . . . . . . . . 17
273	272	nn0cnd 10879	. . . . . . . . . . . . . . . 16
274	262, 273	sylan2 474	. . . . . . . . . . . . . . 15
275	263, 274	mulneg1d 10034	. . . . . . . . . . . . . 14
276	267, 275	eqtrd 2498	. . . . . . . . . . . . 13
277	276	sumeq2dv 13525	. . . . . . . . . . . 12
278	247, 277	syl5eq 2510	. . . . . . . . . . 11
279	157, 273	mulcld 9637	. . . . . . . . . . . . 13
280	262, 279	sylan2 474	. . . . . . . . . . . 12
281	176, 280	fsumneg 13602	. . . . . . . . . . 11
282	238, 278, 281	3eqtrd 2502	. . . . . . . . . 10
283	282	oveq2d 6312	. . . . . . . . 9
284	140	a1i 11	. . . . . . . . . . . . 13
285	284	sselda 3503	. . . . . . . . . . . 12
286	285, 165	syldan 470	. . . . . . . . . . 11
287	176, 286	fsumcl 13555	. . . . . . . . . 10
288	285, 279	syldan 470	. . . . . . . . . . 11
289	176, 288	fsumcl 13555	. . . . . . . . . 10
290	287, 289	negsubd 9960	. . . . . . . . 9
291	166, 283, 290	3eqtrd 2502	. . . . . . . 8
292	291	adantr 465	. . . . . . 7
293	102, 135, 292	3eqtr4d 2508	. . . . . 6
294	293	ex 434	. . . . 5
295	294	ralrimdva 2875	. . . 4
296		ineq1 3692	. . . . . . . 8
297	296	fveq2d 5875	. . . . . . 7
298	67, 297	oveq12d 6314	. . . . . 6
299		ineq1 3692	. . . . . . . . 9
300	299	fveq2d 5875	. . . . . . . 8
301	300	oveq2d 6312	. . . . . . 7
302	301	sumeq2sdv 13526	. . . . . 6
303	298, 302	eqeq12d 2479	. . . . 5
304	303	cbvralv 3084	. . . 4
305	295, 304	syl6ibr 227	. . 3
306	16, 24, 38, 46, 66, 305	findcard2s 7781	. 2
307		fveq2 5871	. . . . 5
308		ineq1 3692	. . . . . 6
309	308	fveq2d 5875	. . . . 5
310	307, 309	oveq12d 6314	. . . 4
311		simpl 457	. . . . . . . 8
312	311	ineq1d 3698	. . . . . . 7
313	312	fveq2d 5875	. . . . . 6
314	313	oveq2d 6312	. . . . 5
315	314	sumeq2dv 13525	. . . 4
316	310, 315	eqeq12d 2479	. . 3
317	316	rspccva 3209	. 2
318	306, 317	sylan 471	1

Syntax hints:  -.wn 3  ->wi 4  /\wa 369  =wceq 1395  e.wcel 1818  A.wral 2807  cvv 3109  \cdif 3472  u.cun 3473  i^icin 3474  C_wss 3475  c0 3784  ~Pcpw 4012  {csn 4029  U.cuni 4249  |^|cint 4286  e.cmpt 4510  `cfv 5593  (class class class)co 6296  cfn 7536  cc 9511  0cc0 9513  1c1 9514  caddc 9516  cmul 9518  cmin 9828  -ucneg 9829  cn0 10820  cexp 12166  chash 12405  sum_csu 13508

This theorem is referenced by:  incexc  13649

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-rep 4563  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592  ax-inf2 8079  ax-cnex 9569  ax-resscn 9570  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-addrcl 9574  ax-mulcl 9575  ax-mulrcl 9576  ax-mulcom 9577  ax-addass 9578  ax-mulass 9579  ax-distr 9580  ax-i2m1 9581  ax-1ne0 9582  ax-1rid 9583  ax-rnegex 9584  ax-rrecex 9585  ax-cnre 9586  ax-pre-lttri 9587  ax-pre-lttrn 9588  ax-pre-ltadd 9589  ax-pre-mulgt0 9590  ax-pre-sup 9591

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-fal 1401  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-pss 3491  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-tp 4034  df-op 4036  df-uni 4250  df-int 4287  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-se 4844  df-we 4845  df-ord 4886  df-on 4887  df-lim 4888  df-suc 4889  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-isom 5602  df-riota 6257  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6701  df-1st 6800  df-2nd 6801  df-recs 7061  df-rdg 7095  df-1o 7149  df-2o 7150  df-oadd 7153  df-er 7330  df-map 7441  df-en 7537  df-dom 7538  df-sdom 7539  df-fin 7540  df-sup 7921  df-oi 7956  df-card 8341  df-cda 8569  df-pnf 9651  df-mnf 9652  df-xr 9653  df-ltxr 9654  df-le 9655  df-sub 9830  df-neg 9831  df-div 10232  df-nn 10562  df-2 10619  df-3 10620  df-n0 10821  df-z 10890  df-uz 11111  df-rp 11250  df-fz 11702  df-fzo 11825  df-seq 12108  df-exp 12167  df-hash 12406  df-cj 12932  df-re 12933  df-im 12934  df-sqrt 13068  df-abs 13069  df-clim 13311  df-sum 13509