isercolllem2 - Metamath Proof Explorer

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

Theorem isercolllem2 13437

Description: Lemma for isercoll 13439. (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 11703	. . . . . . . 8
2	1	a1i 11	. . . . . . 7 $/\$
3		cnvimass 5348	. . . . . . . . 9
4		isercoll.g	. . . . . . . . . . 11
5	4	adantr 465	. . . . . . . . . 10 $/\$
6		fdm 5726	. . . . . . . . . 10
7	5, 6	syl 16	. . . . . . . . 9 $/\$
8	3, 7	syl5sseq 3545	. . . . . . . 8 $/\$
9	8	sseld 3496	. . . . . . 7 $/\$
10		id 22	. . . . . . . . . . 11
11		nnuz 11106	. . . . . . . . . . 11
12	10, 11	syl6eleq 2558	. . . . . . . . . 10
13		ltso 9654	. . . . . . . . . . . . . 14
14	13	a1i 11	. . . . . . . . . . . . 13 $/\$
15		fzfid 12039	. . . . . . . . . . . . . . 15 $/\$
16		ffun 5724	. . . . . . . . . . . . . . . . 17
17		funimacnv 5651	. . . . . . . . . . . . . . . . 17
18	5, 16, 17	3syl 20	. . . . . . . . . . . . . . . 16 $/\$
19		inss1 3711	. . . . . . . . . . . . . . . 16
20	18, 19	syl6eqss 3547	. . . . . . . . . . . . . . 15 $/\$
21		ssfi 7730	. . . . . . . . . . . . . . 15 $/\$
22	15, 20, 21	syl2anc 661	. . . . . . . . . . . . . 14 $/\$
23		ssid 3516	. . . . . . . . . . . . . . . . . . . . 21
24		isercoll.z	. . . . . . . . . . . . . . . . . . . . . 22
25		isercoll.m	. . . . . . . . . . . . . . . . . . . . . 22
26		isercoll.i	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
27	24, 25, 4, 26	isercolllem1 13436	. . . . . . . . . . . . . . . . . . . . 21 $/\$
28	23, 27	mpan2 671	. . . . . . . . . . . . . . . . . . . 20
29		ffn 5722	. . . . . . . . . . . . . . . . . . . . 21
30		fnresdm 5681	. . . . . . . . . . . . . . . . . . . . 21
31		isoeq1 6194	. . . . . . . . . . . . . . . . . . . . 21
32	4, 29, 30, 31	4syl 21	. . . . . . . . . . . . . . . . . . . 20
33	28, 32	mpbid 210	. . . . . . . . . . . . . . . . . . 19
34		isof1o 6200	. . . . . . . . . . . . . . . . . . 19
35		f1ocnv 5819	. . . . . . . . . . . . . . . . . . 19
36		f1ofun 5809	. . . . . . . . . . . . . . . . . . 19
37	33, 34, 35, 36	4syl 21	. . . . . . . . . . . . . . . . . 18
38		df-f1 5584	. . . . . . . . . . . . . . . . . 18 $/\$
39	4, 37, 38	sylanbrc 664	. . . . . . . . . . . . . . . . 17
40	39	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
41		nnex 10531	. . . . . . . . . . . . . . . . 17
42		ssexg 4586	. . . . . . . . . . . . . . . . 17 $/\$
43	8, 41, 42	sylancl 662	. . . . . . . . . . . . . . . 16 $/\$
44		f1imaeng 7565	. . . . . . . . . . . . . . . 16 $/\$ $/\$
45	40, 8, 43, 44	syl3anc 1223	. . . . . . . . . . . . . . 15 $/\$
46	45	ensymd 7556	. . . . . . . . . . . . . 14 $/\$
47		enfii 7727	. . . . . . . . . . . . . 14 $/\$
48	22, 46, 47	syl2anc 661	. . . . . . . . . . . . 13 $/\$
49		1nn 10536	. . . . . . . . . . . . . . . 16
50	49	a1i 11	. . . . . . . . . . . . . . 15 $/\$
51		ffvelrn 6010	. . . . . . . . . . . . . . . . . . 19 $/\$
52	4, 49, 51	sylancl 662	. . . . . . . . . . . . . . . . . 18
53	52, 24	syl6eleq 2558	. . . . . . . . . . . . . . . . 17
54	53	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
55		simpr 461	. . . . . . . . . . . . . . . 16 $/\$
56		elfzuzb 11671	. . . . . . . . . . . . . . . 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 915	. . . . . . . . . . . . . 14 $/\$
62		ne0i 3784	. . . . . . . . . . . . . 14
63	61, 62	syl 16	. . . . . . . . . . . . 13 $/\$
64		nnssre 10529	. . . . . . . . . . . . . 14
65	8, 64	syl6ss 3509	. . . . . . . . . . . . 13 $/\$
66		fisupcl 7916	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
67	14, 48, 63, 65, 66	syl13anc 1225	. . . . . . . . . . . 12 $/\$
68	8, 67	sseldd 3498	. . . . . . . . . . 11 $/\$
69	68	nnzd 10954	. . . . . . . . . 10 $/\$
70		elfz5 11669	. . . . . . . . . 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 11679	. . . . . . . . . . . . . . 15
77	75, 76	syl 16	. . . . . . . . . . . . . 14 $/\$
78	77	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$
79		uzssz 11090	. . . . . . . . . . . . . . . . 17
80	24, 79	eqsstri 3527	. . . . . . . . . . . . . . . 16
81		zssre 10860	. . . . . . . . . . . . . . . 16
82	80, 81	sstri 3506	. . . . . . . . . . . . . . 15
83	5	ffvelrnda 6012	. . . . . . . . . . . . . . 15 $/\$ $/\$
84	82, 83	sseldi 3495	. . . . . . . . . . . . . 14 $/\$ $/\$
85	5, 68	ffvelrnd 6013	. . . . . . . . . . . . . . . 16 $/\$
86	85	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$
87	82, 86	sseldi 3495	. . . . . . . . . . . . . 14 $/\$ $/\$
88		eluzelz 11080	. . . . . . . . . . . . . . . 16
89	88	ad2antlr 726	. . . . . . . . . . . . . . 15 $/\$ $/\$
90	81, 89	sseldi 3495	. . . . . . . . . . . . . 14 $/\$ $/\$
91		letr 9667	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
92	84, 87, 90, 91	syl3anc 1223	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
93	78, 92	mpan2d 674	. . . . . . . . . . . 12 $/\$ $/\$
94	33	ad2antrr 725	. . . . . . . . . . . . 13 $/\$ $/\$
95	64	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
96		ressxr 9626	. . . . . . . . . . . . . 14
97	95, 96	syl6ss 3509	. . . . . . . . . . . . 13 $/\$ $/\$
98		imassrn 5339	. . . . . . . . . . . . . . . 16
99	4	ad2antrr 725	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
100		frn 5728	. . . . . . . . . . . . . . . . 17
101	99, 100	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
102	98, 101	syl5ss 3508	. . . . . . . . . . . . . . 15 $/\$ $/\$
103	102, 82	syl6ss 3509	. . . . . . . . . . . . . 14 $/\$ $/\$
104	103, 96	syl6ss 3509	. . . . . . . . . . . . 13 $/\$ $/\$
105		simpr 461	. . . . . . . . . . . . 13 $/\$ $/\$
106	68	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$
107		leisorel 12462	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
108	94, 97, 104, 105, 106, 107	syl122anc 1232	. . . . . . . . . . . 12 $/\$ $/\$
109	83, 24	syl6eleq 2558	. . . . . . . . . . . . 13 $/\$ $/\$
110		elfz5 11669	. . . . . . . . . . . . 13 $/\$
111	109, 89, 110	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$
112	93, 108, 111	3imtr4d 268	. . . . . . . . . . 11 $/\$ $/\$
113		elpreima 5992	. . . . . . . . . . . . 13 $/\$
114	113	baibd 902	. . . . . . . . . . . 12 $/\$
115	58, 114	sylan 471	. . . . . . . . . . 11 $/\$ $/\$
116	112, 115	sylibrd 234	. . . . . . . . . 10 $/\$ $/\$
117		fimaxre2 10480	. . . . . . . . . . . . 13 $/\$
118	65, 48, 117	syl2anc 661	. . . . . . . . . . . 12 $/\$
119		suprub 10493	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
120	119	ex 434	. . . . . . . . . . . 12 $/\$ $/\$
121	65, 63, 118, 120	syl3anc 1223	. . . . . . . . . . 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 2457	. . . . 5 $/\$
128	127	fveq2d 5861	. . . 4 $/\$
129	68	nnnn0d 10841	. . . . 5 $/\$
130		hashfz1 12374	. . . . 5
131	129, 130	syl 16	. . . 4 $/\$
132		hashen 12375	. . . . . 6 $/\$
133	48, 22, 132	syl2anc 661	. . . . 5 $/\$
134	46, 133	mpbird 232	. . . 4 $/\$
135	128, 131, 134	3eqtr3d 2509	. . 3 $/\$
136	135	oveq2d 6291	. 2 $/\$
137	136, 127	eqtr3d 2503	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1374

wcel 1762

wne 2655

wral 2807

wrex 2808

cvv 3106

cin 3468

wss 3469

c0 3778 class class class wbr 4440

wor 4792

ccnv 4991

cdm 4992

crn 4993

cres 4994

cima 4995

wfun 5573

wfn 5574

wf 5575

wf1 5576

wf1o 5578

cfv 5579

wiso 5580 (class class class)co 6275

cen 7503

cfn 7506

csup 7889

cr 9480

c1 9482

caddc 9484

cxr 9616

clt 9617

cle 9618

cn 10525

cn0 10784

cz 10853

cuz 11071

cfz 11661

chash 12360

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1714 ax-7 1734 ax-8 1764 ax-9 1766 ax-10 1781 ax-11 1786 ax-12 1798 ax-13 1961 ax-ext 2438 ax-rep 4551 ax-sep 4561 ax-nul 4569 ax-pow 4618 ax-pr 4679 ax-un 6567 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 370 df-an 371 df-3or 969 df-3an 970 df-tru 1377 df-ex 1592 df-nf 1595 df-sb 1707 df-eu 2272 df-mo 2273 df-clab 2446 df-cleq 2452 df-clel 2455 df-nfc 2610 df-ne 2657 df-nel 2658 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3108 df-sbc 3325 df-csb 3429 df-dif 3472 df-un 3474 df-in 3476 df-ss 3483 df-pss 3485 df-nul 3779 df-if 3933 df-pw 4005 df-sn 4021 df-pr 4023 df-tp 4025 df-op 4027 df-uni 4239 df-int 4276 df-iun 4320 df-br 4441 df-opab 4499 df-mpt 4500 df-tr 4534 df-eprel 4784 df-id 4788 df-po 4793 df-so 4794 df-fr 4831 df-we 4833 df-ord 4874 df-on 4875 df-lim 4876 df-suc 4877 df-xp 4998 df-rel 4999 df-cnv 5000 df-co 5001 df-dm 5002 df-rn 5003 df-res 5004 df-ima 5005 df-iota 5542 df-fun 5581 df-fn 5582 df-f 5583 df-f1 5584 df-fo 5585 df-f1o 5586 df-fv 5587 df-isom 5588 df-riota 6236 df-ov 6278 df-oprab 6279 df-mpt2 6280 df-om 6672 df-1st 6774 df-2nd 6775 df-recs 7032 df-rdg 7066 df-1o 7120 df-er 7301 df-en 7507 df-dom 7508 df-sdom 7509 df-fin 7510 df-sup 7890 df-card 8309 df-pnf 9619 df-mnf 9620 df-xr 9621 df-ltxr 9622 df-le 9623 df-sub 9796 df-neg 9797 df-nn 10526 df-n0 10785 df-z 10854 df-uz 11072 df-fz 11662 df-hash 12361

This theorem is referenced by: isercolllem3 13438

W3C validator