isercolllem2 - Metamath Proof Explorer

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

Theorem isercolllem2 13247

Description: Lemma for isercoll 13249. (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 11581	. . . . . . . 8
2	1	a1i 11	. . . . . . 7 $/\$
3		cnvimass 5289	. . . . . . . . 9
4		isercoll.g	. . . . . . . . . . 11
5	4	adantr 465	. . . . . . . . . 10 $/\$
6		fdm 5663	. . . . . . . . . 10
7	5, 6	syl 16	. . . . . . . . 9 $/\$
8	3, 7	syl5sseq 3504	. . . . . . . 8 $/\$
9	8	sseld 3455	. . . . . . 7 $/\$
10		id 22	. . . . . . . . . . 11
11		nnuz 10999	. . . . . . . . . . 11
12	10, 11	syl6eleq 2549	. . . . . . . . . 10
13		ltso 9558	. . . . . . . . . . . . . 14
14	13	a1i 11	. . . . . . . . . . . . 13 $/\$
15		fzfid 11898	. . . . . . . . . . . . . . 15 $/\$
16		ffun 5661	. . . . . . . . . . . . . . . . 17
17		funimacnv 5590	. . . . . . . . . . . . . . . . 17
18	5, 16, 17	3syl 20	. . . . . . . . . . . . . . . 16 $/\$
19		inss1 3670	. . . . . . . . . . . . . . . 16
20	18, 19	syl6eqss 3506	. . . . . . . . . . . . . . 15 $/\$
21		ssfi 7636	. . . . . . . . . . . . . . 15 $/\$
22	15, 20, 21	syl2anc 661	. . . . . . . . . . . . . 14 $/\$
23		ssid 3475	. . . . . . . . . . . . . . . . . . . . 21
24		isercoll.z	. . . . . . . . . . . . . . . . . . . . . 22
25		isercoll.m	. . . . . . . . . . . . . . . . . . . . . 22
26		isercoll.i	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
27	24, 25, 4, 26	isercolllem1 13246	. . . . . . . . . . . . . . . . . . . . 21 $/\$
28	23, 27	mpan2 671	. . . . . . . . . . . . . . . . . . . 20
29		ffn 5659	. . . . . . . . . . . . . . . . . . . . 21
30		fnresdm 5620	. . . . . . . . . . . . . . . . . . . . 21
31		isoeq1 6111	. . . . . . . . . . . . . . . . . . . . 21
32	4, 29, 30, 31	4syl 21	. . . . . . . . . . . . . . . . . . . 20
33	28, 32	mpbid 210	. . . . . . . . . . . . . . . . . . 19
34		isof1o 6117	. . . . . . . . . . . . . . . . . . 19
35		f1ocnv 5753	. . . . . . . . . . . . . . . . . . 19
36		f1ofun 5743	. . . . . . . . . . . . . . . . . . 19
37	33, 34, 35, 36	4syl 21	. . . . . . . . . . . . . . . . . 18
38		df-f1 5523	. . . . . . . . . . . . . . . . . 18 $/\$
39	4, 37, 38	sylanbrc 664	. . . . . . . . . . . . . . . . 17
40	39	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
41		nnex 10431	. . . . . . . . . . . . . . . . 17
42		ssexg 4538	. . . . . . . . . . . . . . . . 17 $/\$
43	8, 41, 42	sylancl 662	. . . . . . . . . . . . . . . 16 $/\$
44		f1imaeng 7471	. . . . . . . . . . . . . . . 16 $/\$ $/\$
45	40, 8, 43, 44	syl3anc 1219	. . . . . . . . . . . . . . 15 $/\$
46	45	ensymd 7462	. . . . . . . . . . . . . 14 $/\$
47		enfii 7633	. . . . . . . . . . . . . 14 $/\$
48	22, 46, 47	syl2anc 661	. . . . . . . . . . . . 13 $/\$
49		1nn 10436	. . . . . . . . . . . . . . . 16
50	49	a1i 11	. . . . . . . . . . . . . . 15 $/\$
51		ffvelrn 5942	. . . . . . . . . . . . . . . . . . 19 $/\$
52	4, 49, 51	sylancl 662	. . . . . . . . . . . . . . . . . 18
53	52, 24	syl6eleq 2549	. . . . . . . . . . . . . . . . 17
54	53	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
55		simpr 461	. . . . . . . . . . . . . . . 16 $/\$
56		elfzuzb 11550	. . . . . . . . . . . . . . . 16 $/\$
57	54, 55, 56	sylanbrc 664	. . . . . . . . . . . . . . 15 $/\$
58	5, 29	syl 16	. . . . . . . . . . . . . . . 16 $/\$
59		elpreima 5924	. . . . . . . . . . . . . . . 16 $/\$
60	58, 59	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$
61	50, 57, 60	mpbir2and 913	. . . . . . . . . . . . . 14 $/\$
62		ne0i 3743	. . . . . . . . . . . . . 14
63	61, 62	syl 16	. . . . . . . . . . . . 13 $/\$
64		nnssre 10429	. . . . . . . . . . . . . 14
65	8, 64	syl6ss 3468	. . . . . . . . . . . . 13 $/\$
66		fisupcl 7820	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
67	14, 48, 63, 65, 66	syl13anc 1221	. . . . . . . . . . . 12 $/\$
68	8, 67	sseldd 3457	. . . . . . . . . . 11 $/\$
69	68	nnzd 10849	. . . . . . . . . 10 $/\$
70		elfz5 11548	. . . . . . . . . 10 $/\$
71	12, 69, 70	syl2anr 478	. . . . . . . . 9 $/\$ $/\$
72		elpreima 5924	. . . . . . . . . . . . . . . . . 18 $/\$
73	58, 72	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
74	67, 73	mpbid 210	. . . . . . . . . . . . . . . 16 $/\$ $/\$
75	74	simprd 463	. . . . . . . . . . . . . . 15 $/\$
76		elfzle2 11558	. . . . . . . . . . . . . . 15
77	75, 76	syl 16	. . . . . . . . . . . . . 14 $/\$
78	77	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$
79		uzssz 10983	. . . . . . . . . . . . . . . . 17
80	24, 79	eqsstri 3486	. . . . . . . . . . . . . . . 16
81		zssre 10756	. . . . . . . . . . . . . . . 16
82	80, 81	sstri 3465	. . . . . . . . . . . . . . 15
83	5	ffvelrnda 5944	. . . . . . . . . . . . . . 15 $/\$ $/\$
84	82, 83	sseldi 3454	. . . . . . . . . . . . . 14 $/\$ $/\$
85	5, 68	ffvelrnd 5945	. . . . . . . . . . . . . . . 16 $/\$
86	85	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$
87	82, 86	sseldi 3454	. . . . . . . . . . . . . 14 $/\$ $/\$
88		eluzelz 10973	. . . . . . . . . . . . . . . 16
89	88	ad2antlr 726	. . . . . . . . . . . . . . 15 $/\$ $/\$
90	81, 89	sseldi 3454	. . . . . . . . . . . . . 14 $/\$ $/\$
91		letr 9571	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
92	84, 87, 90, 91	syl3anc 1219	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
93	78, 92	mpan2d 674	. . . . . . . . . . . 12 $/\$ $/\$
94	33	ad2antrr 725	. . . . . . . . . . . . 13 $/\$ $/\$
95	64	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
96		ressxr 9530	. . . . . . . . . . . . . 14
97	95, 96	syl6ss 3468	. . . . . . . . . . . . 13 $/\$ $/\$
98		imassrn 5280	. . . . . . . . . . . . . . . 16
99	4	ad2antrr 725	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
100		frn 5665	. . . . . . . . . . . . . . . . 17
101	99, 100	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
102	98, 101	syl5ss 3467	. . . . . . . . . . . . . . 15 $/\$ $/\$
103	102, 82	syl6ss 3468	. . . . . . . . . . . . . 14 $/\$ $/\$
104	103, 96	syl6ss 3468	. . . . . . . . . . . . 13 $/\$ $/\$
105		simpr 461	. . . . . . . . . . . . 13 $/\$ $/\$
106	68	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$
107		leisorel 12317	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
108	94, 97, 104, 105, 106, 107	syl122anc 1228	. . . . . . . . . . . 12 $/\$ $/\$
109	83, 24	syl6eleq 2549	. . . . . . . . . . . . 13 $/\$ $/\$
110		elfz5 11548	. . . . . . . . . . . . 13 $/\$
111	109, 89, 110	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$
112	93, 108, 111	3imtr4d 268	. . . . . . . . . . 11 $/\$ $/\$
113		elpreima 5924	. . . . . . . . . . . . 13 $/\$
114	113	baibd 900	. . . . . . . . . . . 12 $/\$
115	58, 114	sylan 471	. . . . . . . . . . 11 $/\$ $/\$
116	112, 115	sylibrd 234	. . . . . . . . . 10 $/\$ $/\$
117		fimaxre2 10381	. . . . . . . . . . . . 13 $/\$
118	65, 48, 117	syl2anc 661	. . . . . . . . . . . 12 $/\$
119		suprub 10394	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
120	119	ex 434	. . . . . . . . . . . 12 $/\$ $/\$
121	65, 63, 118, 120	syl3anc 1219	. . . . . . . . . . 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 2448	. . . . 5 $/\$
128	127	fveq2d 5795	. . . 4 $/\$
129	68	nnnn0d 10739	. . . . 5 $/\$
130		hashfz1 12220	. . . . 5
131	129, 130	syl 16	. . . 4 $/\$
132		hashen 12221	. . . . . 6 $/\$
133	48, 22, 132	syl2anc 661	. . . . 5 $/\$
134	46, 133	mpbird 232	. . . 4 $/\$
135	128, 131, 134	3eqtr3d 2500	. . 3 $/\$
136	135	oveq2d 6208	. 2 $/\$
137	136, 127	eqtr3d 2494	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1370

wcel 1758

wne 2644

wral 2795

wrex 2796

cvv 3070

cin 3427

wss 3428

c0 3737 class class class wbr 4392

wor 4740

ccnv 4939

cdm 4940

crn 4941

cres 4942

cima 4943

wfun 5512

wfn 5513

wf 5514

wf1 5515

wf1o 5517

cfv 5518

wiso 5519 (class class class)co 6192

cen 7409

cfn 7412

csup 7793

cr 9384

c1 9386

caddc 9388

cxr 9520

clt 9521

cle 9522

cn 10425

cn0 10682

cz 10749

cuz 10964

cfz 11540

chash 12206

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 ax-rep 4503 ax-sep 4513 ax-nul 4521 ax-pow 4570 ax-pr 4631 ax-un 6474 ax-cnex 9441 ax-resscn 9442 ax-1cn 9443 ax-icn 9444 ax-addcl 9445 ax-addrcl 9446 ax-mulcl 9447 ax-mulrcl 9448 ax-mulcom 9449 ax-addass 9450 ax-mulass 9451 ax-distr 9452 ax-i2m1 9453 ax-1ne0 9454 ax-1rid 9455 ax-rnegex 9456 ax-rrecex 9457 ax-cnre 9458 ax-pre-lttri 9459 ax-pre-lttrn 9460 ax-pre-ltadd 9461 ax-pre-mulgt0 9462 ax-pre-sup 9463

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2264 df-mo 2265 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2601 df-ne 2646 df-nel 2647 df-ral 2800 df-rex 2801 df-reu 2802 df-rmo 2803 df-rab 2804 df-v 3072 df-sbc 3287 df-csb 3389 df-dif 3431 df-un 3433 df-in 3435 df-ss 3442 df-pss 3444 df-nul 3738 df-if 3892 df-pw 3962 df-sn 3978 df-pr 3980 df-tp 3982 df-op 3984 df-uni 4192 df-int 4229 df-iun 4273 df-br 4393 df-opab 4451 df-mpt 4452 df-tr 4486 df-eprel 4732 df-id 4736 df-po 4741 df-so 4742 df-fr 4779 df-we 4781 df-ord 4822 df-on 4823 df-lim 4824 df-suc 4825 df-xp 4946 df-rel 4947 df-cnv 4948 df-co 4949 df-dm 4950 df-rn 4951 df-res 4952 df-ima 4953 df-iota 5481 df-fun 5520 df-fn 5521 df-f 5522 df-f1 5523 df-fo 5524 df-f1o 5525 df-fv 5526 df-isom 5527 df-riota 6153 df-ov 6195 df-oprab 6196 df-mpt2 6197 df-om 6579 df-1st 6679 df-2nd 6680 df-recs 6934 df-rdg 6968 df-1o 7022 df-er 7203 df-en 7413 df-dom 7414 df-sdom 7415 df-fin 7416 df-sup 7794 df-card 8212 df-pnf 9523 df-mnf 9524 df-xr 9525 df-ltxr 9526 df-le 9527 df-sub 9700 df-neg 9701 df-nn 10426 df-n0 10683 df-z 10750 df-uz 10965 df-fz 11541 df-hash 12207

This theorem is referenced by: isercolllem3 13248

W3C validator