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 13729

Description: Lemma for isercoll 13731. (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 11828	. . . . . . . 8
2	1	a1i 11	. . . . . . 7 $/\$
3		cnvimass 5188	. . . . . . . . 9
4		isercoll.g	. . . . . . . . . . 11
5	4	adantr 467	. . . . . . . . . 10 $/\$
6		fdm 5733	. . . . . . . . . 10
7	5, 6	syl 17	. . . . . . . . 9 $/\$
8	3, 7	syl5sseq 3480	. . . . . . . 8 $/\$
9	8	sseld 3431	. . . . . . 7 $/\$
10		id 22	. . . . . . . . . . 11
11		nnuz 11194	. . . . . . . . . . 11
12	10, 11	syl6eleq 2539	. . . . . . . . . 10
13		ltso 9714	. . . . . . . . . . . . . 14
14	13	a1i 11	. . . . . . . . . . . . 13 $/\$
15		fzfid 12186	. . . . . . . . . . . . . . 15 $/\$
16		ffun 5731	. . . . . . . . . . . . . . . . 17
17		funimacnv 5655	. . . . . . . . . . . . . . . . 17
18	5, 16, 17	3syl 18	. . . . . . . . . . . . . . . 16 $/\$
19		inss1 3652	. . . . . . . . . . . . . . . 16
20	18, 19	syl6eqss 3482	. . . . . . . . . . . . . . 15 $/\$
21		ssfi 7792	. . . . . . . . . . . . . . 15 $/\$
22	15, 20, 21	syl2anc 667	. . . . . . . . . . . . . 14 $/\$
23		ssid 3451	. . . . . . . . . . . . . . . . . . . . 21
24		isercoll.z	. . . . . . . . . . . . . . . . . . . . . 22
25		isercoll.m	. . . . . . . . . . . . . . . . . . . . . 22
26		isercoll.i	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
27	24, 25, 4, 26	isercolllem1 13728	. . . . . . . . . . . . . . . . . . . . 21 $/\$
28	23, 27	mpan2 677	. . . . . . . . . . . . . . . . . . . 20
29		ffn 5728	. . . . . . . . . . . . . . . . . . . . 21
30		fnresdm 5685	. . . . . . . . . . . . . . . . . . . . 21
31		isoeq1 6210	. . . . . . . . . . . . . . . . . . . . 21
32	4, 29, 30, 31	4syl 19	. . . . . . . . . . . . . . . . . . . 20
33	28, 32	mpbid 214	. . . . . . . . . . . . . . . . . . 19
34		isof1o 6216	. . . . . . . . . . . . . . . . . . 19
35		f1ocnv 5826	. . . . . . . . . . . . . . . . . . 19
36		f1ofun 5816	. . . . . . . . . . . . . . . . . . 19
37	33, 34, 35, 36	4syl 19	. . . . . . . . . . . . . . . . . 18
38		df-f1 5587	. . . . . . . . . . . . . . . . . 18 $/\$
39	4, 37, 38	sylanbrc 670	. . . . . . . . . . . . . . . . 17
40	39	adantr 467	. . . . . . . . . . . . . . . 16 $/\$
41		nnex 10615	. . . . . . . . . . . . . . . . 17
42		ssexg 4549	. . . . . . . . . . . . . . . . 17 $/\$
43	8, 41, 42	sylancl 668	. . . . . . . . . . . . . . . 16 $/\$
44		f1imaeng 7629	. . . . . . . . . . . . . . . 16 $/\$ $/\$
45	40, 8, 43, 44	syl3anc 1268	. . . . . . . . . . . . . . 15 $/\$
46	45	ensymd 7620	. . . . . . . . . . . . . 14 $/\$
47		enfii 7789	. . . . . . . . . . . . . 14 $/\$
48	22, 46, 47	syl2anc 667	. . . . . . . . . . . . 13 $/\$
49		1nn 10620	. . . . . . . . . . . . . . . 16
50	49	a1i 11	. . . . . . . . . . . . . . 15 $/\$
51		ffvelrn 6020	. . . . . . . . . . . . . . . . . . 19 $/\$
52	4, 49, 51	sylancl 668	. . . . . . . . . . . . . . . . . 18
53	52, 24	syl6eleq 2539	. . . . . . . . . . . . . . . . 17
54	53	adantr 467	. . . . . . . . . . . . . . . 16 $/\$
55		simpr 463	. . . . . . . . . . . . . . . 16 $/\$
56		elfzuzb 11794	. . . . . . . . . . . . . . . 16 $/\$
57	54, 55, 56	sylanbrc 670	. . . . . . . . . . . . . . 15 $/\$
58	5, 29	syl 17	. . . . . . . . . . . . . . . 16 $/\$
59		elpreima 6002	. . . . . . . . . . . . . . . 16 $/\$
60	58, 59	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$
61	50, 57, 60	mpbir2and 933	. . . . . . . . . . . . . 14 $/\$
62		ne0i 3737	. . . . . . . . . . . . . 14
63	61, 62	syl 17	. . . . . . . . . . . . 13 $/\$
64		nnssre 10613	. . . . . . . . . . . . . 14
65	8, 64	syl6ss 3444	. . . . . . . . . . . . 13 $/\$
66		fisupcl 7985	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
67	14, 48, 63, 65, 66	syl13anc 1270	. . . . . . . . . . . 12 $/\$
68	8, 67	sseldd 3433	. . . . . . . . . . 11 $/\$
69	68	nnzd 11039	. . . . . . . . . 10 $/\$
70		elfz5 11792	. . . . . . . . . 10 $/\$
71	12, 69, 70	syl2anr 481	. . . . . . . . 9 $/\$ $/\$
72		elpreima 6002	. . . . . . . . . . . . . . . . . 18 $/\$
73	58, 72	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
74	67, 73	mpbid 214	. . . . . . . . . . . . . . . 16 $/\$ $/\$
75	74	simprd 465	. . . . . . . . . . . . . . 15 $/\$
76		elfzle2 11803	. . . . . . . . . . . . . . 15
77	75, 76	syl 17	. . . . . . . . . . . . . 14 $/\$
78	77	adantr 467	. . . . . . . . . . . . 13 $/\$ $/\$
79		uzssz 11178	. . . . . . . . . . . . . . . . 17
80	24, 79	eqsstri 3462	. . . . . . . . . . . . . . . 16
81		zssre 10944	. . . . . . . . . . . . . . . 16
82	80, 81	sstri 3441	. . . . . . . . . . . . . . 15
83	5	ffvelrnda 6022	. . . . . . . . . . . . . . 15 $/\$ $/\$
84	82, 83	sseldi 3430	. . . . . . . . . . . . . 14 $/\$ $/\$
85	5, 68	ffvelrnd 6023	. . . . . . . . . . . . . . . 16 $/\$
86	85	adantr 467	. . . . . . . . . . . . . . 15 $/\$ $/\$
87	82, 86	sseldi 3430	. . . . . . . . . . . . . 14 $/\$ $/\$
88		eluzelz 11168	. . . . . . . . . . . . . . . 16
89	88	ad2antlr 733	. . . . . . . . . . . . . . 15 $/\$ $/\$
90	81, 89	sseldi 3430	. . . . . . . . . . . . . 14 $/\$ $/\$
91		letr 9727	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
92	84, 87, 90, 91	syl3anc 1268	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
93	78, 92	mpan2d 680	. . . . . . . . . . . 12 $/\$ $/\$
94	33	ad2antrr 732	. . . . . . . . . . . . 13 $/\$ $/\$
95	64	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
96		ressxr 9684	. . . . . . . . . . . . . 14
97	95, 96	syl6ss 3444	. . . . . . . . . . . . 13 $/\$ $/\$
98		imassrn 5179	. . . . . . . . . . . . . . . 16
99	4	ad2antrr 732	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
100		frn 5735	. . . . . . . . . . . . . . . . 17
101	99, 100	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$
102	98, 101	syl5ss 3443	. . . . . . . . . . . . . . 15 $/\$ $/\$
103	102, 82	syl6ss 3444	. . . . . . . . . . . . . 14 $/\$ $/\$
104	103, 96	syl6ss 3444	. . . . . . . . . . . . 13 $/\$ $/\$
105		simpr 463	. . . . . . . . . . . . 13 $/\$ $/\$
106	68	adantr 467	. . . . . . . . . . . . 13 $/\$ $/\$
107		leisorel 12623	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
108	94, 97, 104, 105, 106, 107	syl122anc 1277	. . . . . . . . . . . 12 $/\$ $/\$
109	83, 24	syl6eleq 2539	. . . . . . . . . . . . 13 $/\$ $/\$
110		elfz5 11792	. . . . . . . . . . . . 13 $/\$
111	109, 89, 110	syl2anc 667	. . . . . . . . . . . 12 $/\$ $/\$
112	93, 108, 111	3imtr4d 272	. . . . . . . . . . 11 $/\$ $/\$
113		elpreima 6002	. . . . . . . . . . . . 13 $/\$
114	113	baibd 920	. . . . . . . . . . . 12 $/\$
115	58, 114	sylan 474	. . . . . . . . . . 11 $/\$ $/\$
116	112, 115	sylibrd 238	. . . . . . . . . 10 $/\$ $/\$
117		fimaxre2 10552	. . . . . . . . . . . . 13 $/\$
118	65, 48, 117	syl2anc 667	. . . . . . . . . . . 12 $/\$
119		suprub 10570	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
120	119	ex 436	. . . . . . . . . . . 12 $/\$ $/\$
121	65, 63, 118, 120	syl3anc 1268	. . . . . . . . . . 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 2449	. . . . 5 $/\$
128	127	fveq2d 5869	. . . 4 $/\$
129	68	nnnn0d 10925	. . . . 5 $/\$
130		hashfz1 12529	. . . . 5
131	129, 130	syl 17	. . . 4 $/\$
132		hashen 12530	. . . . . 6 $/\$
133	48, 22, 132	syl2anc 667	. . . . 5 $/\$
134	46, 133	mpbird 236	. . . 4 $/\$
135	128, 131, 134	3eqtr3d 2493	. . 3 $/\$
136	135	oveq2d 6306	. 2 $/\$
137	136, 127	eqtr3d 2487	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1444

wcel 1887

wne 2622

wral 2737

wrex 2738

cvv 3045

cin 3403

wss 3404

c0 3731 class class class wbr 4402

wor 4754

ccnv 4833

cdm 4834

crn 4835

cres 4836

cima 4837

wfun 5576

wfn 5577

wf 5578

wf1 5579

wf1o 5581

cfv 5582

wiso 5583 (class class class)co 6290

cen 7566

cfn 7569

csup 7954

cr 9538

c1 9540

caddc 9542

cxr 9674

clt 9675

cle 9676

cn 10609

cn0 10869

cz 10937

cuz 11159

cfz 11784

chash 12515

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-rep 4515 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-cnex 9595 ax-resscn 9596 ax-1cn 9597 ax-icn 9598 ax-addcl 9599 ax-addrcl 9600 ax-mulcl 9601 ax-mulrcl 9602 ax-mulcom 9603 ax-addass 9604 ax-mulass 9605 ax-distr 9606 ax-i2m1 9607 ax-1ne0 9608 ax-1rid 9609 ax-rnegex 9610 ax-rrecex 9611 ax-cnre 9612 ax-pre-lttri 9613 ax-pre-lttrn 9614 ax-pre-ltadd 9615 ax-pre-mulgt0 9616 ax-pre-sup 9617

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-reu 2744 df-rmo 2745 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-tp 3973 df-op 3975 df-uni 4199 df-int 4235 df-iun 4280 df-br 4403 df-opab 4462 df-mpt 4463 df-tr 4498 df-eprel 4745 df-id 4749 df-po 4755 df-so 4756 df-fr 4793 df-we 4795 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-pred 5380 df-ord 5426 df-on 5427 df-lim 5428 df-suc 5429 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-isom 5591 df-riota 6252 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-om 6693 df-1st 6793 df-2nd 6794 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-1o 7182 df-er 7363 df-en 7570 df-dom 7571 df-sdom 7572 df-fin 7573 df-sup 7956 df-card 8373 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 df-sub 9862 df-neg 9863 df-nn 10610 df-n0 10870 df-z 10938 df-uz 11160 df-fz 11785 df-hash 12516

This theorem is referenced by: isercolllem3 13730

W3C validator