isercolllem2 - Metamath Proof Explorer

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

Theorem isercolllem2 13806

Description: Lemma for isercoll 13808. (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 11854	. . . . . . . 8
2	1	a1i 11	. . . . . . 7 $/\$
3		cnvimass 5194	. . . . . . . . 9
4		isercoll.g	. . . . . . . . . . 11
5	4	adantr 472	. . . . . . . . . 10 $/\$
6		fdm 5745	. . . . . . . . . 10
7	5, 6	syl 17	. . . . . . . . 9 $/\$
8	3, 7	syl5sseq 3466	. . . . . . . 8 $/\$
9	8	sseld 3417	. . . . . . 7 $/\$
10		id 22	. . . . . . . . . . 11
11		nnuz 11218	. . . . . . . . . . 11
12	10, 11	syl6eleq 2559	. . . . . . . . . 10
13		ltso 9732	. . . . . . . . . . . . . 14
14	13	a1i 11	. . . . . . . . . . . . 13 $/\$
15		fzfid 12224	. . . . . . . . . . . . . . 15 $/\$
16		ffun 5742	. . . . . . . . . . . . . . . . 17
17		funimacnv 5665	. . . . . . . . . . . . . . . . 17
18	5, 16, 17	3syl 18	. . . . . . . . . . . . . . . 16 $/\$
19		inss1 3643	. . . . . . . . . . . . . . . 16
20	18, 19	syl6eqss 3468	. . . . . . . . . . . . . . 15 $/\$
21		ssfi 7810	. . . . . . . . . . . . . . 15 $/\$
22	15, 20, 21	syl2anc 673	. . . . . . . . . . . . . 14 $/\$
23		ssid 3437	. . . . . . . . . . . . . . . . . . . . 21
24		isercoll.z	. . . . . . . . . . . . . . . . . . . . . 22
25		isercoll.m	. . . . . . . . . . . . . . . . . . . . . 22
26		isercoll.i	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
27	24, 25, 4, 26	isercolllem1 13805	. . . . . . . . . . . . . . . . . . . . 21 $/\$
28	23, 27	mpan2 685	. . . . . . . . . . . . . . . . . . . 20
29		ffn 5739	. . . . . . . . . . . . . . . . . . . . 21
30		fnresdm 5695	. . . . . . . . . . . . . . . . . . . . 21
31		isoeq1 6228	. . . . . . . . . . . . . . . . . . . . 21
32	4, 29, 30, 31	4syl 19	. . . . . . . . . . . . . . . . . . . 20
33	28, 32	mpbid 215	. . . . . . . . . . . . . . . . . . 19
34		isof1o 6234	. . . . . . . . . . . . . . . . . . 19
35		f1ocnv 5840	. . . . . . . . . . . . . . . . . . 19
36		f1ofun 5830	. . . . . . . . . . . . . . . . . . 19
37	33, 34, 35, 36	4syl 19	. . . . . . . . . . . . . . . . . 18
38		df-f1 5594	. . . . . . . . . . . . . . . . . 18 $/\$
39	4, 37, 38	sylanbrc 677	. . . . . . . . . . . . . . . . 17
40	39	adantr 472	. . . . . . . . . . . . . . . 16 $/\$
41		nnex 10637	. . . . . . . . . . . . . . . . 17
42		ssexg 4542	. . . . . . . . . . . . . . . . 17 $/\$
43	8, 41, 42	sylancl 675	. . . . . . . . . . . . . . . 16 $/\$
44		f1imaeng 7647	. . . . . . . . . . . . . . . 16 $/\$ $/\$
45	40, 8, 43, 44	syl3anc 1292	. . . . . . . . . . . . . . 15 $/\$
46	45	ensymd 7638	. . . . . . . . . . . . . 14 $/\$
47		enfii 7807	. . . . . . . . . . . . . 14 $/\$
48	22, 46, 47	syl2anc 673	. . . . . . . . . . . . 13 $/\$
49		1nn 10642	. . . . . . . . . . . . . . . 16
50	49	a1i 11	. . . . . . . . . . . . . . 15 $/\$
51		ffvelrn 6035	. . . . . . . . . . . . . . . . . . 19 $/\$
52	4, 49, 51	sylancl 675	. . . . . . . . . . . . . . . . . 18
53	52, 24	syl6eleq 2559	. . . . . . . . . . . . . . . . 17
54	53	adantr 472	. . . . . . . . . . . . . . . 16 $/\$
55		simpr 468	. . . . . . . . . . . . . . . 16 $/\$
56		elfzuzb 11820	. . . . . . . . . . . . . . . 16 $/\$
57	54, 55, 56	sylanbrc 677	. . . . . . . . . . . . . . 15 $/\$
58	5, 29	syl 17	. . . . . . . . . . . . . . . 16 $/\$
59		elpreima 6017	. . . . . . . . . . . . . . . 16 $/\$
60	58, 59	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$
61	50, 57, 60	mpbir2and 936	. . . . . . . . . . . . . 14 $/\$
62		ne0i 3728	. . . . . . . . . . . . . 14
63	61, 62	syl 17	. . . . . . . . . . . . 13 $/\$
64		nnssre 10635	. . . . . . . . . . . . . 14
65	8, 64	syl6ss 3430	. . . . . . . . . . . . 13 $/\$
66		fisupcl 8003	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
67	14, 48, 63, 65, 66	syl13anc 1294	. . . . . . . . . . . 12 $/\$
68	8, 67	sseldd 3419	. . . . . . . . . . 11 $/\$
69	68	nnzd 11062	. . . . . . . . . 10 $/\$
70		elfz5 11818	. . . . . . . . . 10 $/\$
71	12, 69, 70	syl2anr 486	. . . . . . . . 9 $/\$ $/\$
72		elpreima 6017	. . . . . . . . . . . . . . . . . 18 $/\$
73	58, 72	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
74	67, 73	mpbid 215	. . . . . . . . . . . . . . . 16 $/\$ $/\$
75	74	simprd 470	. . . . . . . . . . . . . . 15 $/\$
76		elfzle2 11829	. . . . . . . . . . . . . . 15
77	75, 76	syl 17	. . . . . . . . . . . . . 14 $/\$
78	77	adantr 472	. . . . . . . . . . . . 13 $/\$ $/\$
79		uzssz 11202	. . . . . . . . . . . . . . . . 17
80	24, 79	eqsstri 3448	. . . . . . . . . . . . . . . 16
81		zssre 10968	. . . . . . . . . . . . . . . 16
82	80, 81	sstri 3427	. . . . . . . . . . . . . . 15
83	5	ffvelrnda 6037	. . . . . . . . . . . . . . 15 $/\$ $/\$
84	82, 83	sseldi 3416	. . . . . . . . . . . . . 14 $/\$ $/\$
85	5, 68	ffvelrnd 6038	. . . . . . . . . . . . . . . 16 $/\$
86	85	adantr 472	. . . . . . . . . . . . . . 15 $/\$ $/\$
87	82, 86	sseldi 3416	. . . . . . . . . . . . . 14 $/\$ $/\$
88		eluzelz 11192	. . . . . . . . . . . . . . . 16
89	88	ad2antlr 741	. . . . . . . . . . . . . . 15 $/\$ $/\$
90	81, 89	sseldi 3416	. . . . . . . . . . . . . 14 $/\$ $/\$
91		letr 9745	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
92	84, 87, 90, 91	syl3anc 1292	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
93	78, 92	mpan2d 688	. . . . . . . . . . . 12 $/\$ $/\$
94	33	ad2antrr 740	. . . . . . . . . . . . 13 $/\$ $/\$
95	64	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
96		ressxr 9702	. . . . . . . . . . . . . 14
97	95, 96	syl6ss 3430	. . . . . . . . . . . . 13 $/\$ $/\$
98		imassrn 5185	. . . . . . . . . . . . . . . 16
99	4	ad2antrr 740	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
100		frn 5747	. . . . . . . . . . . . . . . . 17
101	99, 100	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$
102	98, 101	syl5ss 3429	. . . . . . . . . . . . . . 15 $/\$ $/\$
103	102, 82	syl6ss 3430	. . . . . . . . . . . . . 14 $/\$ $/\$
104	103, 96	syl6ss 3430	. . . . . . . . . . . . 13 $/\$ $/\$
105		simpr 468	. . . . . . . . . . . . 13 $/\$ $/\$
106	68	adantr 472	. . . . . . . . . . . . 13 $/\$ $/\$
107		leisorel 12664	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
108	94, 97, 104, 105, 106, 107	syl122anc 1301	. . . . . . . . . . . 12 $/\$ $/\$
109	83, 24	syl6eleq 2559	. . . . . . . . . . . . 13 $/\$ $/\$
110		elfz5 11818	. . . . . . . . . . . . 13 $/\$
111	109, 89, 110	syl2anc 673	. . . . . . . . . . . 12 $/\$ $/\$
112	93, 108, 111	3imtr4d 276	. . . . . . . . . . 11 $/\$ $/\$
113		elpreima 6017	. . . . . . . . . . . . 13 $/\$
114	113	baibd 923	. . . . . . . . . . . 12 $/\$
115	58, 114	sylan 479	. . . . . . . . . . 11 $/\$ $/\$
116	112, 115	sylibrd 242	. . . . . . . . . 10 $/\$ $/\$
117		fimaxre2 10574	. . . . . . . . . . . . 13 $/\$
118	65, 48, 117	syl2anc 673	. . . . . . . . . . . 12 $/\$
119		suprub 10592	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
120	119	ex 441	. . . . . . . . . . . 12 $/\$ $/\$
121	65, 63, 118, 120	syl3anc 1292	. . . . . . . . . . 11 $/\$
122	121	adantr 472	. . . . . . . . . 10 $/\$ $/\$
123	116, 122	impbid 195	. . . . . . . . 9 $/\$ $/\$
124	71, 123	bitrd 261	. . . . . . . 8 $/\$ $/\$
125	124	ex 441	. . . . . . 7 $/\$
126	2, 9, 125	pm5.21ndd 361	. . . . . 6 $/\$
127	126	eqrdv 2469	. . . . 5 $/\$
128	127	fveq2d 5883	. . . 4 $/\$
129	68	nnnn0d 10949	. . . . 5 $/\$
130		hashfz1 12567	. . . . 5
131	129, 130	syl 17	. . . 4 $/\$
132		hashen 12568	. . . . . 6 $/\$
133	48, 22, 132	syl2anc 673	. . . . 5 $/\$
134	46, 133	mpbird 240	. . . 4 $/\$
135	128, 131, 134	3eqtr3d 2513	. . 3 $/\$
136	135	oveq2d 6324	. 2 $/\$
137	136, 127	eqtr3d 2507	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 189 $/\$ wa 376 $/\$ w3a 1007

wceq 1452

wcel 1904

wne 2641

wral 2756

wrex 2757

cvv 3031

cin 3389

wss 3390

c0 3722 class class class wbr 4395

wor 4759

ccnv 4838

cdm 4839

crn 4840

cres 4841

cima 4842

wfun 5583

wfn 5584

wf 5585

wf1 5586

wf1o 5588

cfv 5589

wiso 5590 (class class class)co 6308

cen 7584

cfn 7587

csup 7972

cr 9556

c1 9558

caddc 9560

cxr 9692

clt 9693

cle 9694

cn 10631

cn0 10893

cz 10961

cuz 11182

cfz 11810

chash 12553

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-isom 5598 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-om 6712 df-1st 6812 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-er 7381 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-sup 7974 df-card 8391 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-nn 10632 df-n0 10894 df-z 10962 df-uz 11183 df-fz 11811 df-hash 12554

This theorem is referenced by: isercolllem3 13807

W3C validator