isercolllem2 - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > isercolllem2		Structured version Unicode version

Theorem isercolllem2 13135

Description: Lemma for isercoll 13137. (Contributed by Mario Carneiro, 6-Apr-2015.)

**Hypotheses**
Ref	Expression
isercoll.z
isercoll.m
isercoll.g
isercoll.i	$/\$

**Assertion**
Ref	Expression
isercolllem2	$/\$

Distinct variable groups:

Allowed substitution hint:

(

)

Proof of Theorem isercolllem2 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elfznn 11470	. . . . . . . 8
2	1	a1i 11	. . . . . . 7 $/\$
3		cnvimass 5184	. . . . . . . . 9
4		isercoll.g	. . . . . . . . . . 11
5	4	adantr 465	. . . . . . . . . 10 $/\$
6		fdm 5558	. . . . . . . . . 10
7	5, 6	syl 16	. . . . . . . . 9 $/\$
8	3, 7	syl5sseq 3399	. . . . . . . 8 $/\$
9	8	sseld 3350	. . . . . . 7 $/\$
10		id 22	. . . . . . . . . . 11
11		nnuz 10888	. . . . . . . . . . 11
12	10, 11	syl6eleq 2528	. . . . . . . . . 10
13		ltso 9447	. . . . . . . . . . . . . 14
14	13	a1i 11	. . . . . . . . . . . . 13 $/\$
15		fzfid 11787	. . . . . . . . . . . . . . 15 $/\$
16		ffun 5556	. . . . . . . . . . . . . . . . 17
17		funimacnv 5485	. . . . . . . . . . . . . . . . 17
18	5, 16, 17	3syl 20	. . . . . . . . . . . . . . . 16 $/\$
19		inss1 3565	. . . . . . . . . . . . . . . 16
20	18, 19	syl6eqss 3401	. . . . . . . . . . . . . . 15 $/\$
21		ssfi 7525	. . . . . . . . . . . . . . 15 $/\$
22	15, 20, 21	syl2anc 661	. . . . . . . . . . . . . 14 $/\$
23		ssid 3370	. . . . . . . . . . . . . . . . . . . . 21
24		isercoll.z	. . . . . . . . . . . . . . . . . . . . . 22
25		isercoll.m	. . . . . . . . . . . . . . . . . . . . . 22
26		isercoll.i	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
27	24, 25, 4, 26	isercolllem1 13134	. . . . . . . . . . . . . . . . . . . . 21 $/\$
28	23, 27	mpan2 671	. . . . . . . . . . . . . . . . . . . 20
29		ffn 5554	. . . . . . . . . . . . . . . . . . . . 21
30		fnresdm 5515	. . . . . . . . . . . . . . . . . . . . 21
31		isoeq1 6005	. . . . . . . . . . . . . . . . . . . . 21
32	4, 29, 30, 31	4syl 21	. . . . . . . . . . . . . . . . . . . 20
33	28, 32	mpbid 210	. . . . . . . . . . . . . . . . . . 19
34		isof1o 6011	. . . . . . . . . . . . . . . . . . 19
35		f1ocnv 5648	. . . . . . . . . . . . . . . . . . 19
36		f1ofun 5638	. . . . . . . . . . . . . . . . . . 19
37	33, 34, 35, 36	4syl 21	. . . . . . . . . . . . . . . . . 18
38		df-f1 5418	. . . . . . . . . . . . . . . . . 18 $/\$
39	4, 37, 38	sylanbrc 664	. . . . . . . . . . . . . . . . 17
40	39	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
41		nnex 10320	. . . . . . . . . . . . . . . . 17
42		ssexg 4433	. . . . . . . . . . . . . . . . 17 $/\$
43	8, 41, 42	sylancl 662	. . . . . . . . . . . . . . . 16 $/\$
44		f1imaeng 7361	. . . . . . . . . . . . . . . 16 $/\$ $/\$
45	40, 8, 43, 44	syl3anc 1218	. . . . . . . . . . . . . . 15 $/\$
46	45	ensymd 7352	. . . . . . . . . . . . . 14 $/\$
47		enfii 7522	. . . . . . . . . . . . . 14 $/\$
48	22, 46, 47	syl2anc 661	. . . . . . . . . . . . 13 $/\$
49		1nn 10325	. . . . . . . . . . . . . . . 16
50	49	a1i 11	. . . . . . . . . . . . . . 15 $/\$
51		ffvelrn 5836	. . . . . . . . . . . . . . . . . . 19 $/\$
52	4, 49, 51	sylancl 662	. . . . . . . . . . . . . . . . . 18
53	52, 24	syl6eleq 2528	. . . . . . . . . . . . . . . . 17
54	53	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
55		simpr 461	. . . . . . . . . . . . . . . 16 $/\$
56		elfzuzb 11439	. . . . . . . . . . . . . . . 16 $/\$
57	54, 55, 56	sylanbrc 664	. . . . . . . . . . . . . . 15 $/\$
58	5, 29	syl 16	. . . . . . . . . . . . . . . 16 $/\$
59		elpreima 5818	. . . . . . . . . . . . . . . 16 $/\$
60	58, 59	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$
61	50, 57, 60	mpbir2and 913	. . . . . . . . . . . . . 14 $/\$
62		ne0i 3638	. . . . . . . . . . . . . 14
63	61, 62	syl 16	. . . . . . . . . . . . 13 $/\$
64		nnssre 10318	. . . . . . . . . . . . . 14
65	8, 64	syl6ss 3363	. . . . . . . . . . . . 13 $/\$
66		fisupcl 7709	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
67	14, 48, 63, 65, 66	syl13anc 1220	. . . . . . . . . . . 12 $/\$
68	8, 67	sseldd 3352	. . . . . . . . . . 11 $/\$
69	68	nnzd 10738	. . . . . . . . . 10 $/\$
70		elfz5 11437	. . . . . . . . . 10 $/\$
71	12, 69, 70	syl2anr 478	. . . . . . . . 9 $/\$ $/\$
72		elpreima 5818	. . . . . . . . . . . . . . . . . 18 $/\$
73	58, 72	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
74	67, 73	mpbid 210	. . . . . . . . . . . . . . . 16 $/\$ $/\$
75	74	simprd 463	. . . . . . . . . . . . . . 15 $/\$
76		elfzle2 11447	. . . . . . . . . . . . . . 15
77	75, 76	syl 16	. . . . . . . . . . . . . 14 $/\$
78	77	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$
79		uzssz 10872	. . . . . . . . . . . . . . . . 17
80	24, 79	eqsstri 3381	. . . . . . . . . . . . . . . 16
81		zssre 10645	. . . . . . . . . . . . . . . 16
82	80, 81	sstri 3360	. . . . . . . . . . . . . . 15
83	5	ffvelrnda 5838	. . . . . . . . . . . . . . 15 $/\$ $/\$
84	82, 83	sseldi 3349	. . . . . . . . . . . . . 14 $/\$ $/\$
85	5, 68	ffvelrnd 5839	. . . . . . . . . . . . . . . 16 $/\$
86	85	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$
87	82, 86	sseldi 3349	. . . . . . . . . . . . . 14 $/\$ $/\$
88		eluzelz 10862	. . . . . . . . . . . . . . . 16
89	88	ad2antlr 726	. . . . . . . . . . . . . . 15 $/\$ $/\$
90	81, 89	sseldi 3349	. . . . . . . . . . . . . 14 $/\$ $/\$
91		letr 9460	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
92	84, 87, 90, 91	syl3anc 1218	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
93	78, 92	mpan2d 674	. . . . . . . . . . . 12 $/\$ $/\$
94	33	ad2antrr 725	. . . . . . . . . . . . 13 $/\$ $/\$
95	64	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
96		ressxr 9419	. . . . . . . . . . . . . 14
97	95, 96	syl6ss 3363	. . . . . . . . . . . . 13 $/\$ $/\$
98		imassrn 5175	. . . . . . . . . . . . . . . 16
99	4	ad2antrr 725	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
100		frn 5560	. . . . . . . . . . . . . . . . 17
101	99, 100	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
102	98, 101	syl5ss 3362	. . . . . . . . . . . . . . 15 $/\$ $/\$
103	102, 82	syl6ss 3363	. . . . . . . . . . . . . 14 $/\$ $/\$
104	103, 96	syl6ss 3363	. . . . . . . . . . . . 13 $/\$ $/\$
105		simpr 461	. . . . . . . . . . . . 13 $/\$ $/\$
106	68	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$
107		leisorel 12205	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
108	94, 97, 104, 105, 106, 107	syl122anc 1227	. . . . . . . . . . . 12 $/\$ $/\$
109	83, 24	syl6eleq 2528	. . . . . . . . . . . . 13 $/\$ $/\$
110		elfz5 11437	. . . . . . . . . . . . 13 $/\$
111	109, 89, 110	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$
112	93, 108, 111	3imtr4d 268	. . . . . . . . . . 11 $/\$ $/\$
113		elpreima 5818	. . . . . . . . . . . . 13 $/\$
114	113	baibd 900	. . . . . . . . . . . 12 $/\$
115	58, 114	sylan 471	. . . . . . . . . . 11 $/\$ $/\$
116	112, 115	sylibrd 234	. . . . . . . . . 10 $/\$ $/\$
117		fimaxre2 10270	. . . . . . . . . . . . 13 $/\$
118	65, 48, 117	syl2anc 661	. . . . . . . . . . . 12 $/\$
119		suprub 10283	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
120	119	ex 434	. . . . . . . . . . . 12 $/\$ $/\$
121	65, 63, 118, 120	syl3anc 1218	. . . . . . . . . . 11 $/\$
122	121	adantr 465	. . . . . . . . . 10 $/\$ $/\$
123	116, 122	impbid 191	. . . . . . . . 9 $/\$ $/\$
124	71, 123	bitrd 253	. . . . . . . 8 $/\$ $/\$
125	124	ex 434	. . . . . . 7 $/\$
126	2, 9, 125	pm5.21ndd 354	. . . . . 6 $/\$
127	126	eqrdv 2436	. . . . 5 $/\$
128	127	fveq2d 5690	. . . 4 $/\$
129	68	nnnn0d 10628	. . . . 5 $/\$
130		hashfz1 12109	. . . . 5
131	129, 130	syl 16	. . . 4 $/\$
132		hashen 12110	. . . . . 6 $/\$
133	48, 22, 132	syl2anc 661	. . . . 5 $/\$
134	46, 133	mpbird 232	. . . 4 $/\$
135	128, 131, 134	3eqtr3d 2478	. . 3 $/\$
136	135	oveq2d 6102	. 2 $/\$
137	136, 127	eqtr3d 2472	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 965

wceq 1369

wcel 1756

wne 2601

wral 2710

wrex 2711

cvv 2967

cin 3322

wss 3323

c0 3632 class class class wbr 4287

wor 4635

ccnv 4834

cdm 4835

crn 4836

cres 4837

cima 4838

wfun 5407

wfn 5408

wf 5409

wf1 5410

wf1o 5412

cfv 5413

wiso 5414 (class class class)co 6086

cen 7299

cfn 7302

csup 7682

cr 9273

c1 9275

caddc 9277

cxr 9409

clt 9410

cle 9411

cn 10314

cn0 10571

cz 10638

cuz 10853

cfz 11429

chash 12095

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2419 ax-rep 4398 ax-sep 4408 ax-nul 4416 ax-pow 4465 ax-pr 4526 ax-un 6367 ax-cnex 9330 ax-resscn 9331 ax-1cn 9332 ax-icn 9333 ax-addcl 9334 ax-addrcl 9335 ax-mulcl 9336 ax-mulrcl 9337 ax-mulcom 9338 ax-addass 9339 ax-mulass 9340 ax-distr 9341 ax-i2m1 9342 ax-1ne0 9343 ax-1rid 9344 ax-rnegex 9345 ax-rrecex 9346 ax-cnre 9347 ax-pre-lttri 9348 ax-pre-lttrn 9349 ax-pre-ltadd 9350 ax-pre-mulgt0 9351 ax-pre-sup 9352

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2256 df-mo 2257 df-clab 2425 df-cleq 2431 df-clel 2434 df-nfc 2563 df-ne 2603 df-nel 2604 df-ral 2715 df-rex 2716 df-reu 2717 df-rmo 2718 df-rab 2719 df-v 2969 df-sbc 3182 df-csb 3284 df-dif 3326 df-un 3328 df-in 3330 df-ss 3337 df-pss 3339 df-nul 3633 df-if 3787 df-pw 3857 df-sn 3873 df-pr 3875 df-tp 3877 df-op 3879 df-uni 4087 df-int 4124 df-iun 4168 df-br 4288 df-opab 4346 df-mpt 4347 df-tr 4381 df-eprel 4627 df-id 4631 df-po 4636 df-so 4637 df-fr 4674 df-we 4676 df-ord 4717 df-on 4718 df-lim 4719 df-suc 4720 df-xp 4841 df-rel 4842 df-cnv 4843 df-co 4844 df-dm 4845 df-rn 4846 df-res 4847 df-ima 4848 df-iota 5376 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-isom 5422 df-riota 6047 df-ov 6089 df-oprab 6090 df-mpt2 6091 df-om 6472 df-1st 6572 df-2nd 6573 df-recs 6824 df-rdg 6858 df-1o 6912 df-er 7093 df-en 7303 df-dom 7304 df-sdom 7305 df-fin 7306 df-sup 7683 df-card 8101 df-pnf 9412 df-mnf 9413 df-xr 9414 df-ltxr 9415 df-le 9416 df-sub 9589 df-neg 9590 df-nn 10315 df-n0 10572 df-z 10639 df-uz 10854 df-fz 11430 df-hash 12096

This theorem is referenced by: isercolllem3 13136

W3C validator