isercolllem2 - Metamath Proof Explorer

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

Theorem isercolllem2 13722

Description: Lemma for isercoll 13724. (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 11830	. . . . . . . 8
2	1	a1i 11	. . . . . . 7 $/\$
3		cnvimass 5205	. . . . . . . . 9
4		isercoll.g	. . . . . . . . . . 11
5	4	adantr 467	. . . . . . . . . 10 $/\$
6		fdm 5748	. . . . . . . . . 10
7	5, 6	syl 17	. . . . . . . . 9 $/\$
8	3, 7	syl5sseq 3513	. . . . . . . 8 $/\$
9	8	sseld 3464	. . . . . . 7 $/\$
10		id 23	. . . . . . . . . . 11
11		nnuz 11196	. . . . . . . . . . 11
12	10, 11	syl6eleq 2521	. . . . . . . . . 10
13		ltso 9716	. . . . . . . . . . . . . 14
14	13	a1i 11	. . . . . . . . . . . . 13 $/\$
15		fzfid 12187	. . . . . . . . . . . . . . 15 $/\$
16		ffun 5746	. . . . . . . . . . . . . . . . 17
17		funimacnv 5671	. . . . . . . . . . . . . . . . 17
18	5, 16, 17	3syl 18	. . . . . . . . . . . . . . . 16 $/\$
19		inss1 3683	. . . . . . . . . . . . . . . 16
20	18, 19	syl6eqss 3515	. . . . . . . . . . . . . . 15 $/\$
21		ssfi 7796	. . . . . . . . . . . . . . 15 $/\$
22	15, 20, 21	syl2anc 666	. . . . . . . . . . . . . 14 $/\$
23		ssid 3484	. . . . . . . . . . . . . . . . . . . . 21
24		isercoll.z	. . . . . . . . . . . . . . . . . . . . . 22
25		isercoll.m	. . . . . . . . . . . . . . . . . . . . . 22
26		isercoll.i	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
27	24, 25, 4, 26	isercolllem1 13721	. . . . . . . . . . . . . . . . . . . . 21 $/\$
28	23, 27	mpan2 676	. . . . . . . . . . . . . . . . . . . 20
29		ffn 5744	. . . . . . . . . . . . . . . . . . . . 21
30		fnresdm 5701	. . . . . . . . . . . . . . . . . . . . 21
31		isoeq1 6223	. . . . . . . . . . . . . . . . . . . . 21
32	4, 29, 30, 31	4syl 19	. . . . . . . . . . . . . . . . . . . 20
33	28, 32	mpbid 214	. . . . . . . . . . . . . . . . . . 19
34		isof1o 6229	. . . . . . . . . . . . . . . . . . 19
35		f1ocnv 5841	. . . . . . . . . . . . . . . . . . 19
36		f1ofun 5831	. . . . . . . . . . . . . . . . . . 19
37	33, 34, 35, 36	4syl 19	. . . . . . . . . . . . . . . . . 18
38		df-f1 5604	. . . . . . . . . . . . . . . . . 18 $/\$
39	4, 37, 38	sylanbrc 669	. . . . . . . . . . . . . . . . 17
40	39	adantr 467	. . . . . . . . . . . . . . . 16 $/\$
41		nnex 10617	. . . . . . . . . . . . . . . . 17
42		ssexg 4568	. . . . . . . . . . . . . . . . 17 $/\$
43	8, 41, 42	sylancl 667	. . . . . . . . . . . . . . . 16 $/\$
44		f1imaeng 7634	. . . . . . . . . . . . . . . 16 $/\$ $/\$
45	40, 8, 43, 44	syl3anc 1265	. . . . . . . . . . . . . . 15 $/\$
46	45	ensymd 7625	. . . . . . . . . . . . . 14 $/\$
47		enfii 7793	. . . . . . . . . . . . . 14 $/\$
48	22, 46, 47	syl2anc 666	. . . . . . . . . . . . 13 $/\$
49		1nn 10622	. . . . . . . . . . . . . . . 16
50	49	a1i 11	. . . . . . . . . . . . . . 15 $/\$
51		ffvelrn 6033	. . . . . . . . . . . . . . . . . . 19 $/\$
52	4, 49, 51	sylancl 667	. . . . . . . . . . . . . . . . . 18
53	52, 24	syl6eleq 2521	. . . . . . . . . . . . . . . . 17
54	53	adantr 467	. . . . . . . . . . . . . . . 16 $/\$
55		simpr 463	. . . . . . . . . . . . . . . 16 $/\$
56		elfzuzb 11796	. . . . . . . . . . . . . . . 16 $/\$
57	54, 55, 56	sylanbrc 669	. . . . . . . . . . . . . . 15 $/\$
58	5, 29	syl 17	. . . . . . . . . . . . . . . 16 $/\$
59		elpreima 6015	. . . . . . . . . . . . . . . 16 $/\$
60	58, 59	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$
61	50, 57, 60	mpbir2and 931	. . . . . . . . . . . . . 14 $/\$
62		ne0i 3768	. . . . . . . . . . . . . 14
63	61, 62	syl 17	. . . . . . . . . . . . 13 $/\$
64		nnssre 10615	. . . . . . . . . . . . . 14
65	8, 64	syl6ss 3477	. . . . . . . . . . . . 13 $/\$
66		fisupcl 7989	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
67	14, 48, 63, 65, 66	syl13anc 1267	. . . . . . . . . . . 12 $/\$
68	8, 67	sseldd 3466	. . . . . . . . . . 11 $/\$
69	68	nnzd 11041	. . . . . . . . . 10 $/\$
70		elfz5 11794	. . . . . . . . . 10 $/\$
71	12, 69, 70	syl2anr 481	. . . . . . . . 9 $/\$ $/\$
72		elpreima 6015	. . . . . . . . . . . . . . . . . 18 $/\$
73	58, 72	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
74	67, 73	mpbid 214	. . . . . . . . . . . . . . . 16 $/\$ $/\$
75	74	simprd 465	. . . . . . . . . . . . . . 15 $/\$
76		elfzle2 11805	. . . . . . . . . . . . . . 15
77	75, 76	syl 17	. . . . . . . . . . . . . 14 $/\$
78	77	adantr 467	. . . . . . . . . . . . 13 $/\$ $/\$
79		uzssz 11180	. . . . . . . . . . . . . . . . 17
80	24, 79	eqsstri 3495	. . . . . . . . . . . . . . . 16
81		zssre 10946	. . . . . . . . . . . . . . . 16
82	80, 81	sstri 3474	. . . . . . . . . . . . . . 15
83	5	ffvelrnda 6035	. . . . . . . . . . . . . . 15 $/\$ $/\$
84	82, 83	sseldi 3463	. . . . . . . . . . . . . 14 $/\$ $/\$
85	5, 68	ffvelrnd 6036	. . . . . . . . . . . . . . . 16 $/\$
86	85	adantr 467	. . . . . . . . . . . . . . 15 $/\$ $/\$
87	82, 86	sseldi 3463	. . . . . . . . . . . . . 14 $/\$ $/\$
88		eluzelz 11170	. . . . . . . . . . . . . . . 16
89	88	ad2antlr 732	. . . . . . . . . . . . . . 15 $/\$ $/\$
90	81, 89	sseldi 3463	. . . . . . . . . . . . . 14 $/\$ $/\$
91		letr 9729	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
92	84, 87, 90, 91	syl3anc 1265	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
93	78, 92	mpan2d 679	. . . . . . . . . . . 12 $/\$ $/\$
94	33	ad2antrr 731	. . . . . . . . . . . . 13 $/\$ $/\$
95	64	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
96		ressxr 9686	. . . . . . . . . . . . . 14
97	95, 96	syl6ss 3477	. . . . . . . . . . . . 13 $/\$ $/\$
98		imassrn 5196	. . . . . . . . . . . . . . . 16
99	4	ad2antrr 731	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
100		frn 5750	. . . . . . . . . . . . . . . . 17
101	99, 100	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$
102	98, 101	syl5ss 3476	. . . . . . . . . . . . . . 15 $/\$ $/\$
103	102, 82	syl6ss 3477	. . . . . . . . . . . . . 14 $/\$ $/\$
104	103, 96	syl6ss 3477	. . . . . . . . . . . . 13 $/\$ $/\$
105		simpr 463	. . . . . . . . . . . . 13 $/\$ $/\$
106	68	adantr 467	. . . . . . . . . . . . 13 $/\$ $/\$
107		leisorel 12622	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
108	94, 97, 104, 105, 106, 107	syl122anc 1274	. . . . . . . . . . . 12 $/\$ $/\$
109	83, 24	syl6eleq 2521	. . . . . . . . . . . . 13 $/\$ $/\$
110		elfz5 11794	. . . . . . . . . . . . 13 $/\$
111	109, 89, 110	syl2anc 666	. . . . . . . . . . . 12 $/\$ $/\$
112	93, 108, 111	3imtr4d 272	. . . . . . . . . . 11 $/\$ $/\$
113		elpreima 6015	. . . . . . . . . . . . 13 $/\$
114	113	baibd 918	. . . . . . . . . . . 12 $/\$
115	58, 114	sylan 474	. . . . . . . . . . 11 $/\$ $/\$
116	112, 115	sylibrd 238	. . . . . . . . . 10 $/\$ $/\$
117		fimaxre2 10554	. . . . . . . . . . . . 13 $/\$
118	65, 48, 117	syl2anc 666	. . . . . . . . . . . 12 $/\$
119		suprub 10572	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
120	119	ex 436	. . . . . . . . . . . 12 $/\$ $/\$
121	65, 63, 118, 120	syl3anc 1265	. . . . . . . . . . 11 $/\$
122	121	adantr 467	. . . . . . . . . 10 $/\$ $/\$
123	116, 122	impbid 194	. . . . . . . . 9 $/\$ $/\$
124	71, 123	bitrd 257	. . . . . . . 8 $/\$ $/\$
125	124	ex 436	. . . . . . 7 $/\$
126	2, 9, 125	pm5.21ndd 356	. . . . . 6 $/\$
127	126	eqrdv 2420	. . . . 5 $/\$
128	127	fveq2d 5883	. . . 4 $/\$
129	68	nnnn0d 10927	. . . . 5 $/\$
130		hashfz1 12530	. . . . 5
131	129, 130	syl 17	. . . 4 $/\$
132		hashen 12531	. . . . . 6 $/\$
133	48, 22, 132	syl2anc 666	. . . . 5 $/\$
134	46, 133	mpbird 236	. . . 4 $/\$
135	128, 131, 134	3eqtr3d 2472	. . 3 $/\$
136	135	oveq2d 6319	. 2 $/\$
137	136, 127	eqtr3d 2466	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 188 $/\$ wa 371 $/\$ w3a 983

wceq 1438

wcel 1869

wne 2619

wral 2776

wrex 2777

cvv 3082

cin 3436

wss 3437

c0 3762 class class class wbr 4421

wor 4771

ccnv 4850

cdm 4851

crn 4852

cres 4853

cima 4854

wfun 5593

wfn 5594

wf 5595

wf1 5596

wf1o 5598

cfv 5599

wiso 5600 (class class class)co 6303

cen 7572

cfn 7575

csup 7958

cr 9540

c1 9542

caddc 9544

cxr 9676

clt 9677

cle 9678

cn 10611

cn0 10871

cz 10939

cuz 11161

cfz 11786

chash 12516

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1666 ax-4 1679 ax-5 1749 ax-6 1795 ax-7 1840 ax-8 1871 ax-9 1873 ax-10 1888 ax-11 1893 ax-12 1906 ax-13 2054 ax-ext 2401 ax-rep 4534 ax-sep 4544 ax-nul 4553 ax-pow 4600 ax-pr 4658 ax-un 6595 ax-cnex 9597 ax-resscn 9598 ax-1cn 9599 ax-icn 9600 ax-addcl 9601 ax-addrcl 9602 ax-mulcl 9603 ax-mulrcl 9604 ax-mulcom 9605 ax-addass 9606 ax-mulass 9607 ax-distr 9608 ax-i2m1 9609 ax-1ne0 9610 ax-1rid 9611 ax-rnegex 9612 ax-rrecex 9613 ax-cnre 9614 ax-pre-lttri 9615 ax-pre-lttrn 9616 ax-pre-ltadd 9617 ax-pre-mulgt0 9618 ax-pre-sup 9619

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 984 df-3an 985 df-tru 1441 df-ex 1661 df-nf 1665 df-sb 1788 df-eu 2270 df-mo 2271 df-clab 2409 df-cleq 2415 df-clel 2418 df-nfc 2573 df-ne 2621 df-nel 2622 df-ral 2781 df-rex 2782 df-reu 2783 df-rmo 2784 df-rab 2785 df-v 3084 df-sbc 3301 df-csb 3397 df-dif 3440 df-un 3442 df-in 3444 df-ss 3451 df-pss 3453 df-nul 3763 df-if 3911 df-pw 3982 df-sn 3998 df-pr 4000 df-tp 4002 df-op 4004 df-uni 4218 df-int 4254 df-iun 4299 df-br 4422 df-opab 4481 df-mpt 4482 df-tr 4517 df-eprel 4762 df-id 4766 df-po 4772 df-so 4773 df-fr 4810 df-we 4812 df-xp 4857 df-rel 4858 df-cnv 4859 df-co 4860 df-dm 4861 df-rn 4862 df-res 4863 df-ima 4864 df-pred 5397 df-ord 5443 df-on 5444 df-lim 5445 df-suc 5446 df-iota 5563 df-fun 5601 df-fn 5602 df-f 5603 df-f1 5604 df-fo 5605 df-f1o 5606 df-fv 5607 df-isom 5608 df-riota 6265 df-ov 6306 df-oprab 6307 df-mpt2 6308 df-om 6705 df-1st 6805 df-2nd 6806 df-wrecs 7034 df-recs 7096 df-rdg 7134 df-1o 7188 df-er 7369 df-en 7576 df-dom 7577 df-sdom 7578 df-fin 7579 df-sup 7960 df-card 8376 df-pnf 9679 df-mnf 9680 df-xr 9681 df-ltxr 9682 df-le 9683 df-sub 9864 df-neg 9865 df-nn 10612 df-n0 10872 df-z 10940 df-uz 11162 df-fz 11787 df-hash 12517

This theorem is referenced by: isercolllem3 13723

W3C validator