isercolllem2 - Metamath Proof Explorer

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

Theorem isercolllem2 13467

Description: Lemma for isercoll 13469. (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 11723	. . . . . . . 8
2	1	a1i 11	. . . . . . 7 $/\$
3		cnvimass 5347	. . . . . . . . 9
4		isercoll.g	. . . . . . . . . . 11
5	4	adantr 465	. . . . . . . . . 10 $/\$
6		fdm 5725	. . . . . . . . . 10
7	5, 6	syl 16	. . . . . . . . 9 $/\$
8	3, 7	syl5sseq 3537	. . . . . . . 8 $/\$
9	8	sseld 3488	. . . . . . 7 $/\$
10		id 22	. . . . . . . . . . 11
11		nnuz 11125	. . . . . . . . . . 11
12	10, 11	syl6eleq 2541	. . . . . . . . . 10
13		ltso 9668	. . . . . . . . . . . . . 14
14	13	a1i 11	. . . . . . . . . . . . 13 $/\$
15		fzfid 12062	. . . . . . . . . . . . . . 15 $/\$
16		ffun 5723	. . . . . . . . . . . . . . . . 17
17		funimacnv 5650	. . . . . . . . . . . . . . . . 17
18	5, 16, 17	3syl 20	. . . . . . . . . . . . . . . 16 $/\$
19		inss1 3703	. . . . . . . . . . . . . . . 16
20	18, 19	syl6eqss 3539	. . . . . . . . . . . . . . 15 $/\$
21		ssfi 7742	. . . . . . . . . . . . . . 15 $/\$
22	15, 20, 21	syl2anc 661	. . . . . . . . . . . . . 14 $/\$
23		ssid 3508	. . . . . . . . . . . . . . . . . . . . 21
24		isercoll.z	. . . . . . . . . . . . . . . . . . . . . 22
25		isercoll.m	. . . . . . . . . . . . . . . . . . . . . 22
26		isercoll.i	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
27	24, 25, 4, 26	isercolllem1 13466	. . . . . . . . . . . . . . . . . . . . 21 $/\$
28	23, 27	mpan2 671	. . . . . . . . . . . . . . . . . . . 20
29		ffn 5721	. . . . . . . . . . . . . . . . . . . . 21
30		fnresdm 5680	. . . . . . . . . . . . . . . . . . . . 21
31		isoeq1 6200	. . . . . . . . . . . . . . . . . . . . 21
32	4, 29, 30, 31	4syl 21	. . . . . . . . . . . . . . . . . . . 20
33	28, 32	mpbid 210	. . . . . . . . . . . . . . . . . . 19
34		isof1o 6206	. . . . . . . . . . . . . . . . . . 19
35		f1ocnv 5818	. . . . . . . . . . . . . . . . . . 19
36		f1ofun 5808	. . . . . . . . . . . . . . . . . . 19
37	33, 34, 35, 36	4syl 21	. . . . . . . . . . . . . . . . . 18
38		df-f1 5583	. . . . . . . . . . . . . . . . . 18 $/\$
39	4, 37, 38	sylanbrc 664	. . . . . . . . . . . . . . . . 17
40	39	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
41		nnex 10548	. . . . . . . . . . . . . . . . 17
42		ssexg 4583	. . . . . . . . . . . . . . . . 17 $/\$
43	8, 41, 42	sylancl 662	. . . . . . . . . . . . . . . 16 $/\$
44		f1imaeng 7577	. . . . . . . . . . . . . . . 16 $/\$ $/\$
45	40, 8, 43, 44	syl3anc 1229	. . . . . . . . . . . . . . 15 $/\$
46	45	ensymd 7568	. . . . . . . . . . . . . 14 $/\$
47		enfii 7739	. . . . . . . . . . . . . 14 $/\$
48	22, 46, 47	syl2anc 661	. . . . . . . . . . . . 13 $/\$
49		1nn 10553	. . . . . . . . . . . . . . . 16
50	49	a1i 11	. . . . . . . . . . . . . . 15 $/\$
51		ffvelrn 6014	. . . . . . . . . . . . . . . . . . 19 $/\$
52	4, 49, 51	sylancl 662	. . . . . . . . . . . . . . . . . 18
53	52, 24	syl6eleq 2541	. . . . . . . . . . . . . . . . 17
54	53	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
55		simpr 461	. . . . . . . . . . . . . . . 16 $/\$
56		elfzuzb 11691	. . . . . . . . . . . . . . . 16 $/\$
57	54, 55, 56	sylanbrc 664	. . . . . . . . . . . . . . 15 $/\$
58	5, 29	syl 16	. . . . . . . . . . . . . . . 16 $/\$
59		elpreima 5992	. . . . . . . . . . . . . . . 16 $/\$
60	58, 59	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$
61	50, 57, 60	mpbir2and 922	. . . . . . . . . . . . . 14 $/\$
62		ne0i 3776	. . . . . . . . . . . . . 14
63	61, 62	syl 16	. . . . . . . . . . . . 13 $/\$
64		nnssre 10546	. . . . . . . . . . . . . 14
65	8, 64	syl6ss 3501	. . . . . . . . . . . . 13 $/\$
66		fisupcl 7930	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
67	14, 48, 63, 65, 66	syl13anc 1231	. . . . . . . . . . . 12 $/\$
68	8, 67	sseldd 3490	. . . . . . . . . . 11 $/\$
69	68	nnzd 10973	. . . . . . . . . 10 $/\$
70		elfz5 11689	. . . . . . . . . 10 $/\$
71	12, 69, 70	syl2anr 478	. . . . . . . . 9 $/\$ $/\$
72		elpreima 5992	. . . . . . . . . . . . . . . . . 18 $/\$
73	58, 72	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
74	67, 73	mpbid 210	. . . . . . . . . . . . . . . 16 $/\$ $/\$
75	74	simprd 463	. . . . . . . . . . . . . . 15 $/\$
76		elfzle2 11699	. . . . . . . . . . . . . . 15
77	75, 76	syl 16	. . . . . . . . . . . . . 14 $/\$
78	77	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$
79		uzssz 11109	. . . . . . . . . . . . . . . . 17
80	24, 79	eqsstri 3519	. . . . . . . . . . . . . . . 16
81		zssre 10877	. . . . . . . . . . . . . . . 16
82	80, 81	sstri 3498	. . . . . . . . . . . . . . 15
83	5	ffvelrnda 6016	. . . . . . . . . . . . . . 15 $/\$ $/\$
84	82, 83	sseldi 3487	. . . . . . . . . . . . . 14 $/\$ $/\$
85	5, 68	ffvelrnd 6017	. . . . . . . . . . . . . . . 16 $/\$
86	85	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$
87	82, 86	sseldi 3487	. . . . . . . . . . . . . 14 $/\$ $/\$
88		eluzelz 11099	. . . . . . . . . . . . . . . 16
89	88	ad2antlr 726	. . . . . . . . . . . . . . 15 $/\$ $/\$
90	81, 89	sseldi 3487	. . . . . . . . . . . . . 14 $/\$ $/\$
91		letr 9681	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
92	84, 87, 90, 91	syl3anc 1229	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
93	78, 92	mpan2d 674	. . . . . . . . . . . 12 $/\$ $/\$
94	33	ad2antrr 725	. . . . . . . . . . . . 13 $/\$ $/\$
95	64	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
96		ressxr 9640	. . . . . . . . . . . . . 14
97	95, 96	syl6ss 3501	. . . . . . . . . . . . 13 $/\$ $/\$
98		imassrn 5338	. . . . . . . . . . . . . . . 16
99	4	ad2antrr 725	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
100		frn 5727	. . . . . . . . . . . . . . . . 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 461	. . . . . . . . . . . . 13 $/\$ $/\$
106	68	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$
107		leisorel 12488	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
108	94, 97, 104, 105, 106, 107	syl122anc 1238	. . . . . . . . . . . 12 $/\$ $/\$
109	83, 24	syl6eleq 2541	. . . . . . . . . . . . 13 $/\$ $/\$
110		elfz5 11689	. . . . . . . . . . . . 13 $/\$
111	109, 89, 110	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$
112	93, 108, 111	3imtr4d 268	. . . . . . . . . . 11 $/\$ $/\$
113		elpreima 5992	. . . . . . . . . . . . 13 $/\$
114	113	baibd 909	. . . . . . . . . . . 12 $/\$
115	58, 114	sylan 471	. . . . . . . . . . 11 $/\$ $/\$
116	112, 115	sylibrd 234	. . . . . . . . . 10 $/\$ $/\$
117		fimaxre2 10497	. . . . . . . . . . . . 13 $/\$
118	65, 48, 117	syl2anc 661	. . . . . . . . . . . 12 $/\$
119		suprub 10510	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
120	119	ex 434	. . . . . . . . . . . 12 $/\$ $/\$
121	65, 63, 118, 120	syl3anc 1229	. . . . . . . . . . 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 2440	. . . . 5 $/\$
128	127	fveq2d 5860	. . . 4 $/\$
129	68	nnnn0d 10858	. . . . 5 $/\$
130		hashfz1 12398	. . . . 5
131	129, 130	syl 16	. . . 4 $/\$
132		hashen 12399	. . . . . 6 $/\$
133	48, 22, 132	syl2anc 661	. . . . 5 $/\$
134	46, 133	mpbird 232	. . . 4 $/\$
135	128, 131, 134	3eqtr3d 2492	. . 3 $/\$
136	135	oveq2d 6297	. 2 $/\$
137	136, 127	eqtr3d 2486	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1383

wcel 1804

wne 2638

wral 2793

wrex 2794

cvv 3095

cin 3460

wss 3461

c0 3770 class class class wbr 4437

wor 4789

ccnv 4988

cdm 4989

crn 4990

cres 4991

cima 4992

wfun 5572

wfn 5573

wf 5574

wf1 5575

wf1o 5577

cfv 5578

wiso 5579 (class class class)co 6281

cen 7515

cfn 7518

csup 7902

cr 9494

c1 9496

caddc 9498

cxr 9630

clt 9631

cle 9632

cn 10542

cn0 10801

cz 10870

cuz 11090

cfz 11681

chash 12384

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1605 ax-4 1618 ax-5 1691 ax-6 1734 ax-7 1776 ax-8 1806 ax-9 1808 ax-10 1823 ax-11 1828 ax-12 1840 ax-13 1985 ax-ext 2421 ax-rep 4548 ax-sep 4558 ax-nul 4566 ax-pow 4615 ax-pr 4676 ax-un 6577 ax-cnex 9551 ax-resscn 9552 ax-1cn 9553 ax-icn 9554 ax-addcl 9555 ax-addrcl 9556 ax-mulcl 9557 ax-mulrcl 9558 ax-mulcom 9559 ax-addass 9560 ax-mulass 9561 ax-distr 9562 ax-i2m1 9563 ax-1ne0 9564 ax-1rid 9565 ax-rnegex 9566 ax-rrecex 9567 ax-cnre 9568 ax-pre-lttri 9569 ax-pre-lttrn 9570 ax-pre-ltadd 9571 ax-pre-mulgt0 9572 ax-pre-sup 9573

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 975 df-3an 976 df-tru 1386 df-ex 1600 df-nf 1604 df-sb 1727 df-eu 2272 df-mo 2273 df-clab 2429 df-cleq 2435 df-clel 2438 df-nfc 2593 df-ne 2640 df-nel 2641 df-ral 2798 df-rex 2799 df-reu 2800 df-rmo 2801 df-rab 2802 df-v 3097 df-sbc 3314 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-pss 3477 df-nul 3771 df-if 3927 df-pw 3999 df-sn 4015 df-pr 4017 df-tp 4019 df-op 4021 df-uni 4235 df-int 4272 df-iun 4317 df-br 4438 df-opab 4496 df-mpt 4497 df-tr 4531 df-eprel 4781 df-id 4785 df-po 4790 df-so 4791 df-fr 4828 df-we 4830 df-ord 4871 df-on 4872 df-lim 4873 df-suc 4874 df-xp 4995 df-rel 4996 df-cnv 4997 df-co 4998 df-dm 4999 df-rn 5000 df-res 5001 df-ima 5002 df-iota 5541 df-fun 5580 df-fn 5581 df-f 5582 df-f1 5583 df-fo 5584 df-f1o 5585 df-fv 5586 df-isom 5587 df-riota 6242 df-ov 6284 df-oprab 6285 df-mpt2 6286 df-om 6686 df-1st 6785 df-2nd 6786 df-recs 7044 df-rdg 7078 df-1o 7132 df-er 7313 df-en 7519 df-dom 7520 df-sdom 7521 df-fin 7522 df-sup 7903 df-card 8323 df-pnf 9633 df-mnf 9634 df-xr 9635 df-ltxr 9636 df-le 9637 df-sub 9812 df-neg 9813 df-nn 10543 df-n0 10802 df-z 10871 df-uz 11091 df-fz 11682 df-hash 12385

This theorem is referenced by: isercolllem3 13468

W3C validator