isercolllem2 - Metamath Proof Explorer

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

Theorem isercolllem2 13570

Description: Lemma for isercoll 13572. (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 11717	. . . . . . . 8
2	1	a1i 11	. . . . . . 7 $/\$
3		cnvimass 5345	. . . . . . . . 9
4		isercoll.g	. . . . . . . . . . 11
5	4	adantr 463	. . . . . . . . . 10 $/\$
6		fdm 5717	. . . . . . . . . 10
7	5, 6	syl 16	. . . . . . . . 9 $/\$
8	3, 7	syl5sseq 3537	. . . . . . . 8 $/\$
9	8	sseld 3488	. . . . . . 7 $/\$
10		id 22	. . . . . . . . . . 11
11		nnuz 11117	. . . . . . . . . . 11
12	10, 11	syl6eleq 2552	. . . . . . . . . 10
13		ltso 9654	. . . . . . . . . . . . . 14
14	13	a1i 11	. . . . . . . . . . . . 13 $/\$
15		fzfid 12065	. . . . . . . . . . . . . . 15 $/\$
16		ffun 5715	. . . . . . . . . . . . . . . . 17
17		funimacnv 5642	. . . . . . . . . . . . . . . . 17
18	5, 16, 17	3syl 20	. . . . . . . . . . . . . . . 16 $/\$
19		inss1 3704	. . . . . . . . . . . . . . . 16
20	18, 19	syl6eqss 3539	. . . . . . . . . . . . . . 15 $/\$
21		ssfi 7733	. . . . . . . . . . . . . . 15 $/\$
22	15, 20, 21	syl2anc 659	. . . . . . . . . . . . . 14 $/\$
23		ssid 3508	. . . . . . . . . . . . . . . . . . . . 21
24		isercoll.z	. . . . . . . . . . . . . . . . . . . . . 22
25		isercoll.m	. . . . . . . . . . . . . . . . . . . . . 22
26		isercoll.i	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
27	24, 25, 4, 26	isercolllem1 13569	. . . . . . . . . . . . . . . . . . . . 21 $/\$
28	23, 27	mpan2 669	. . . . . . . . . . . . . . . . . . . 20
29		ffn 5713	. . . . . . . . . . . . . . . . . . . . 21
30		fnresdm 5672	. . . . . . . . . . . . . . . . . . . . 21
31		isoeq1 6190	. . . . . . . . . . . . . . . . . . . . 21
32	4, 29, 30, 31	4syl 21	. . . . . . . . . . . . . . . . . . . 20
33	28, 32	mpbid 210	. . . . . . . . . . . . . . . . . . 19
34		isof1o 6196	. . . . . . . . . . . . . . . . . . 19
35		f1ocnv 5810	. . . . . . . . . . . . . . . . . . 19
36		f1ofun 5800	. . . . . . . . . . . . . . . . . . 19
37	33, 34, 35, 36	4syl 21	. . . . . . . . . . . . . . . . . 18
38		df-f1 5575	. . . . . . . . . . . . . . . . . 18 $/\$
39	4, 37, 38	sylanbrc 662	. . . . . . . . . . . . . . . . 17
40	39	adantr 463	. . . . . . . . . . . . . . . 16 $/\$
41		nnex 10537	. . . . . . . . . . . . . . . . 17
42		ssexg 4583	. . . . . . . . . . . . . . . . 17 $/\$
43	8, 41, 42	sylancl 660	. . . . . . . . . . . . . . . 16 $/\$
44		f1imaeng 7568	. . . . . . . . . . . . . . . 16 $/\$ $/\$
45	40, 8, 43, 44	syl3anc 1226	. . . . . . . . . . . . . . 15 $/\$
46	45	ensymd 7559	. . . . . . . . . . . . . 14 $/\$
47		enfii 7730	. . . . . . . . . . . . . 14 $/\$
48	22, 46, 47	syl2anc 659	. . . . . . . . . . . . 13 $/\$
49		1nn 10542	. . . . . . . . . . . . . . . 16
50	49	a1i 11	. . . . . . . . . . . . . . 15 $/\$
51		ffvelrn 6005	. . . . . . . . . . . . . . . . . . 19 $/\$
52	4, 49, 51	sylancl 660	. . . . . . . . . . . . . . . . . 18
53	52, 24	syl6eleq 2552	. . . . . . . . . . . . . . . . 17
54	53	adantr 463	. . . . . . . . . . . . . . . 16 $/\$
55		simpr 459	. . . . . . . . . . . . . . . 16 $/\$
56		elfzuzb 11685	. . . . . . . . . . . . . . . 16 $/\$
57	54, 55, 56	sylanbrc 662	. . . . . . . . . . . . . . 15 $/\$
58	5, 29	syl 16	. . . . . . . . . . . . . . . 16 $/\$
59		elpreima 5983	. . . . . . . . . . . . . . . 16 $/\$
60	58, 59	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$
61	50, 57, 60	mpbir2and 920	. . . . . . . . . . . . . 14 $/\$
62		ne0i 3789	. . . . . . . . . . . . . 14
63	61, 62	syl 16	. . . . . . . . . . . . 13 $/\$
64		nnssre 10535	. . . . . . . . . . . . . 14
65	8, 64	syl6ss 3501	. . . . . . . . . . . . 13 $/\$
66		fisupcl 7919	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
67	14, 48, 63, 65, 66	syl13anc 1228	. . . . . . . . . . . 12 $/\$
68	8, 67	sseldd 3490	. . . . . . . . . . 11 $/\$
69	68	nnzd 10964	. . . . . . . . . 10 $/\$
70		elfz5 11683	. . . . . . . . . 10 $/\$
71	12, 69, 70	syl2anr 476	. . . . . . . . 9 $/\$ $/\$
72		elpreima 5983	. . . . . . . . . . . . . . . . . 18 $/\$
73	58, 72	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
74	67, 73	mpbid 210	. . . . . . . . . . . . . . . 16 $/\$ $/\$
75	74	simprd 461	. . . . . . . . . . . . . . 15 $/\$
76		elfzle2 11693	. . . . . . . . . . . . . . 15
77	75, 76	syl 16	. . . . . . . . . . . . . 14 $/\$
78	77	adantr 463	. . . . . . . . . . . . 13 $/\$ $/\$
79		uzssz 11101	. . . . . . . . . . . . . . . . 17
80	24, 79	eqsstri 3519	. . . . . . . . . . . . . . . 16
81		zssre 10867	. . . . . . . . . . . . . . . 16
82	80, 81	sstri 3498	. . . . . . . . . . . . . . 15
83	5	ffvelrnda 6007	. . . . . . . . . . . . . . 15 $/\$ $/\$
84	82, 83	sseldi 3487	. . . . . . . . . . . . . 14 $/\$ $/\$
85	5, 68	ffvelrnd 6008	. . . . . . . . . . . . . . . 16 $/\$
86	85	adantr 463	. . . . . . . . . . . . . . 15 $/\$ $/\$
87	82, 86	sseldi 3487	. . . . . . . . . . . . . 14 $/\$ $/\$
88		eluzelz 11091	. . . . . . . . . . . . . . . 16
89	88	ad2antlr 724	. . . . . . . . . . . . . . 15 $/\$ $/\$
90	81, 89	sseldi 3487	. . . . . . . . . . . . . 14 $/\$ $/\$
91		letr 9667	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
92	84, 87, 90, 91	syl3anc 1226	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
93	78, 92	mpan2d 672	. . . . . . . . . . . 12 $/\$ $/\$
94	33	ad2antrr 723	. . . . . . . . . . . . 13 $/\$ $/\$
95	64	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
96		ressxr 9626	. . . . . . . . . . . . . 14
97	95, 96	syl6ss 3501	. . . . . . . . . . . . 13 $/\$ $/\$
98		imassrn 5336	. . . . . . . . . . . . . . . 16
99	4	ad2antrr 723	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
100		frn 5719	. . . . . . . . . . . . . . . . 17
101	99, 100	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
102	98, 101	syl5ss 3500	. . . . . . . . . . . . . . 15 $/\$ $/\$
103	102, 82	syl6ss 3501	. . . . . . . . . . . . . 14 $/\$ $/\$
104	103, 96	syl6ss 3501	. . . . . . . . . . . . 13 $/\$ $/\$
105		simpr 459	. . . . . . . . . . . . 13 $/\$ $/\$
106	68	adantr 463	. . . . . . . . . . . . 13 $/\$ $/\$
107		leisorel 12493	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
108	94, 97, 104, 105, 106, 107	syl122anc 1235	. . . . . . . . . . . 12 $/\$ $/\$
109	83, 24	syl6eleq 2552	. . . . . . . . . . . . 13 $/\$ $/\$
110		elfz5 11683	. . . . . . . . . . . . 13 $/\$
111	109, 89, 110	syl2anc 659	. . . . . . . . . . . 12 $/\$ $/\$
112	93, 108, 111	3imtr4d 268	. . . . . . . . . . 11 $/\$ $/\$
113		elpreima 5983	. . . . . . . . . . . . 13 $/\$
114	113	baibd 907	. . . . . . . . . . . 12 $/\$
115	58, 114	sylan 469	. . . . . . . . . . 11 $/\$ $/\$
116	112, 115	sylibrd 234	. . . . . . . . . 10 $/\$ $/\$
117		fimaxre2 10486	. . . . . . . . . . . . 13 $/\$
118	65, 48, 117	syl2anc 659	. . . . . . . . . . . 12 $/\$
119		suprub 10499	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
120	119	ex 432	. . . . . . . . . . . 12 $/\$ $/\$
121	65, 63, 118, 120	syl3anc 1226	. . . . . . . . . . 11 $/\$
122	121	adantr 463	. . . . . . . . . 10 $/\$ $/\$
123	116, 122	impbid 191	. . . . . . . . 9 $/\$ $/\$
124	71, 123	bitrd 253	. . . . . . . 8 $/\$ $/\$
125	124	ex 432	. . . . . . 7 $/\$
126	2, 9, 125	pm5.21ndd 352	. . . . . 6 $/\$
127	126	eqrdv 2451	. . . . 5 $/\$
128	127	fveq2d 5852	. . . 4 $/\$
129	68	nnnn0d 10848	. . . . 5 $/\$
130		hashfz1 12401	. . . . 5
131	129, 130	syl 16	. . . 4 $/\$
132		hashen 12402	. . . . . 6 $/\$
133	48, 22, 132	syl2anc 659	. . . . 5 $/\$
134	46, 133	mpbird 232	. . . 4 $/\$
135	128, 131, 134	3eqtr3d 2503	. . 3 $/\$
136	135	oveq2d 6286	. 2 $/\$
137	136, 127	eqtr3d 2497	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 367 $/\$ w3a 971

wceq 1398

wcel 1823

wne 2649

wral 2804

wrex 2805

cvv 3106

cin 3460

wss 3461

c0 3783 class class class wbr 4439

wor 4788

ccnv 4987

cdm 4988

crn 4989

cres 4990

cima 4991

wfun 5564

wfn 5565

wf 5566

wf1 5567

wf1o 5569

cfv 5570

wiso 5571 (class class class)co 6270

cen 7506

cfn 7509

csup 7892

cr 9480

c1 9482

caddc 9484

cxr 9616

clt 9617

cle 9618

cn 10531

cn0 10791

cz 10860

cuz 11082

cfz 11675

chash 12387

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1623 ax-4 1636 ax-5 1709 ax-6 1752 ax-7 1795 ax-8 1825 ax-9 1827 ax-10 1842 ax-11 1847 ax-12 1859 ax-13 2004 ax-ext 2432 ax-rep 4550 ax-sep 4560 ax-nul 4568 ax-pow 4615 ax-pr 4676 ax-un 6565 ax-cnex 9537 ax-resscn 9538 ax-1cn 9539 ax-icn 9540 ax-addcl 9541 ax-addrcl 9542 ax-mulcl 9543 ax-mulrcl 9544 ax-mulcom 9545 ax-addass 9546 ax-mulass 9547 ax-distr 9548 ax-i2m1 9549 ax-1ne0 9550 ax-1rid 9551 ax-rnegex 9552 ax-rrecex 9553 ax-cnre 9554 ax-pre-lttri 9555 ax-pre-lttrn 9556 ax-pre-ltadd 9557 ax-pre-mulgt0 9558 ax-pre-sup 9559

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1401 df-ex 1618 df-nf 1622 df-sb 1745 df-eu 2288 df-mo 2289 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2651 df-nel 2652 df-ral 2809 df-rex 2810 df-reu 2811 df-rmo 2812 df-rab 2813 df-v 3108 df-sbc 3325 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-pss 3477 df-nul 3784 df-if 3930 df-pw 4001 df-sn 4017 df-pr 4019 df-tp 4021 df-op 4023 df-uni 4236 df-int 4272 df-iun 4317 df-br 4440 df-opab 4498 df-mpt 4499 df-tr 4533 df-eprel 4780 df-id 4784 df-po 4789 df-so 4790 df-fr 4827 df-we 4829 df-ord 4870 df-on 4871 df-lim 4872 df-suc 4873 df-xp 4994 df-rel 4995 df-cnv 4996 df-co 4997 df-dm 4998 df-rn 4999 df-res 5000 df-ima 5001 df-iota 5534 df-fun 5572 df-fn 5573 df-f 5574 df-f1 5575 df-fo 5576 df-f1o 5577 df-fv 5578 df-isom 5579 df-riota 6232 df-ov 6273 df-oprab 6274 df-mpt2 6275 df-om 6674 df-1st 6773 df-2nd 6774 df-recs 7034 df-rdg 7068 df-1o 7122 df-er 7303 df-en 7510 df-dom 7511 df-sdom 7512 df-fin 7513 df-sup 7893 df-card 8311 df-pnf 9619 df-mnf 9620 df-xr 9621 df-ltxr 9622 df-le 9623 df-sub 9798 df-neg 9799 df-nn 10532 df-n0 10792 df-z 10861 df-uz 11083 df-fz 11676 df-hash 12388

This theorem is referenced by: isercolllem3 13571

W3C validator