opnmbllem - Metamath Proof Explorer

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

Theorem opnmbllem 21040

Description: Lemma for opnmbl 21041. (Contributed by Mario Carneiro, 26-Mar-2015.)

**Hypothesis**
Ref	Expression
dyadmbl.1

**Assertion**
Ref	Expression
opnmbllem

Distinct variable groups:

Proof of Theorem opnmbllem Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 5688	. . . . . . . . 9
2	1	sseq1d 3380	. . . . . . . 8
3	2	elrab 3114	. . . . . . 7 $/\$
4		simprr 751	. . . . . . . 8 $/\$ $/\$
5		fvex 5698	. . . . . . . . 9
6	5	elpw 3863	. . . . . . . 8
7	4, 6	sylibr 212	. . . . . . 7 $/\$ $/\$
8	3, 7	sylan2b 472	. . . . . 6 $/\$
9	8	ralrimiva 2797	. . . . 5
10		iccf 11384	. . . . . . 7
11		ffun 5558	. . . . . . 7
12	10, 11	ax-mp 5	. . . . . 6
13		ssrab2 3434	. . . . . . . 8
14		dyadmbl.1	. . . . . . . . . . 11
15	14	dyadf 21030	. . . . . . . . . 10
16		frn 5562	. . . . . . . . . 10
17	15, 16	ax-mp 5	. . . . . . . . 9
18		inss2 3568	. . . . . . . . . 10
19		rexpssxrxp 9424	. . . . . . . . . 10
20	18, 19	sstri 3362	. . . . . . . . 9
21	17, 20	sstri 3362	. . . . . . . 8
22	13, 21	sstri 3362	. . . . . . 7
23	10	fdmi 5561	. . . . . . 7
24	22, 23	sseqtr4i 3386	. . . . . 6
25		funimass4 5739	. . . . . 6 $/\$
26	12, 24, 25	mp2an 667	. . . . 5
27	9, 26	sylibr 212	. . . 4
28		sspwuni 4253	. . . 4
29	27, 28	sylib 196	. . 3
30		eqid 2441	. . . . . . . 8
31	30	rexmet 20327	. . . . . . 7
32		eqid 2441	. . . . . . . . 9
33	30, 32	tgioo 20332	. . . . . . . 8
34	33	mopni2 20027	. . . . . . 7 $/\$ $/\$
35	31, 34	mp3an1 1296	. . . . . 6 $/\$
36		elssuni 4118	. . . . . . . . . . . 12
37		uniretop 20300	. . . . . . . . . . . 12
38	36, 37	syl6sseqr 3400	. . . . . . . . . . 11
39	38	sselda 3353	. . . . . . . . . 10 $/\$
40		rpre 10993	. . . . . . . . . 10
41	30	bl2ioo 20328	. . . . . . . . . 10 $/\$
42	39, 40, 41	syl2an 474	. . . . . . . . 9 $/\$ $/\$
43	42	sseq1d 3380	. . . . . . . 8 $/\$ $/\$
44		2re 10387	. . . . . . . . . . . 12
45		1lt2 10484	. . . . . . . . . . . 12
46		expnlbnd 11990	. . . . . . . . . . . 12 $/\$ $/\$
47	44, 45, 46	mp3an23 1301	. . . . . . . . . . 11
48	47	ad2antrl 722	. . . . . . . . . 10 $/\$ $/\$ $/\$
49	39	ad2antrr 720	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
50		2nn 10475	. . . . . . . . . . . . . . . . . . 19
51		nnnn0 10582	. . . . . . . . . . . . . . . . . . . 20
52	51	ad2antrl 722	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
53		nnexpcl 11874	. . . . . . . . . . . . . . . . . . 19 $/\$
54	50, 52, 53	sylancr 658	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
55	54	nnred 10333	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
56	49, 55	remulcld 9410	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
57		fllelt 11643	. . . . . . . . . . . . . . . 16 $/\$
58	56, 57	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59	58	simpld 456	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
60		reflcl 11642	. . . . . . . . . . . . . . . 16
61	56, 60	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
62	54	nngt0d 10361	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
63		ledivmul2 10205	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
64	61, 49, 55, 62, 63	syl112anc 1217	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
65	59, 64	mpbird 232	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
66		peano2re 9538	. . . . . . . . . . . . . . . 16
67	61, 66	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
68	67, 54	nndivred 10366	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
69	58	simprd 460	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
70		ltmuldiv 10198	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
71	49, 67, 55, 62, 70	syl112anc 1217	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
72	69, 71	mpbid 210	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
73	49, 68, 72	ltled 9518	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
74	61, 54	nndivred 10366	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
75		elicc2 11356	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
76	74, 68, 75	syl2anc 656	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
77	49, 65, 73, 76	mpbir3and 1166	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
78	56	flcld 11644	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
79	14	dyadval 21031	. . . . . . . . . . . . . . 15 $/\$
80	78, 52, 79	syl2anc 656	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
81	80	fveq2d 5692	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
82		df-ov 6093	. . . . . . . . . . . . 13
83	81, 82	syl6eqr 2491	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
84	77, 83	eleqtrrd 2518	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
85		ffn 5556	. . . . . . . . . . . . . . . 16
86	15, 85	ax-mp 5	. . . . . . . . . . . . . . 15
87		fnovrn 6237	. . . . . . . . . . . . . . 15 $/\$ $/\$
88	86, 87	mp3an1 1296	. . . . . . . . . . . . . 14 $/\$
89	78, 52, 88	syl2anc 656	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
90		simplrl 754	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
91	90	rpred 11023	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
92	49, 91	resubcld 9772	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
93	92	rexrd 9429	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
94	49, 91	readdcld 9409	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
95	94	rexrd 9429	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
96	74, 91	readdcld 9409	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
97	61	recnd 9408	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
98		1cnd 9398	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
99	55	recnd 9408	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
100	54	nnne0d 10362	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
101	97, 98, 99, 100	divdird 10141	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
102	54	nnrecred 10363	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
103		simprr 751	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
104	102, 91, 74, 103	ltadd2dd 9526	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
105	101, 104	eqbrtrd 4309	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
106	49, 68, 96, 72, 105	lttrd 9528	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
107	49, 91, 74	ltsubaddd 9931	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
108	106, 107	mpbird 232	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
109	49, 102	readdcld 9409	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
110	74, 49, 102, 65	leadd1dd 9949	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
111	101, 110	eqbrtrd 4309	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
112	102, 91, 49, 103	ltadd2dd 9526	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
113	68, 109, 94, 111, 112	lelttrd 9525	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
114		iccssioo 11360	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
115	93, 95, 108, 113, 114	syl22anc 1214	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
116	83, 115	eqsstrd 3387	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
117		simplrr 755	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
118	116, 117	sstrd 3363	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
119		fveq2 5688	. . . . . . . . . . . . . . 15
120	119	sseq1d 3380	. . . . . . . . . . . . . 14
121	120	elrab 3114	. . . . . . . . . . . . 13 $/\$
122	89, 118, 121	sylanbrc 659	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
123		funfvima2 5950	. . . . . . . . . . . . 13 $/\$
124	12, 24, 123	mp2an 667	. . . . . . . . . . . 12
125	122, 124	syl 16	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
126		elunii 4093	. . . . . . . . . . 11 $/\$
127	84, 125, 126	syl2anc 656	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
128	48, 127	rexlimddv 2843	. . . . . . . . 9 $/\$ $/\$ $/\$
129	128	expr 612	. . . . . . . 8 $/\$ $/\$
130	43, 129	sylbid 215	. . . . . . 7 $/\$ $/\$
131	130	rexlimdva 2839	. . . . . 6 $/\$
132	35, 131	mpd 15	. . . . 5 $/\$
133	132	ex 434	. . . 4
134	133	ssrdv 3359	. . 3
135	29, 134	eqssd 3370	. 2
136		fveq2 5688	. . . . . . 7
137	136	sseq1d 3380	. . . . . 6
138		equequ1 1741	. . . . . 6
139	137, 138	imbi12d 320	. . . . 5
140	139	ralbidv 2733	. . . 4
141	140	cbvrabv 2969	. . 3
142	13	a1i 11	. . 3
143	14, 141, 142	dyadmbl 21039	. 2
144	135, 143	eqeltrrd 2516	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1364

wcel 1761

wral 2713

wrex 2714

crab 2717

cin 3324

wss 3325

cpw 3857

cop 3880

cuni 4088 class class class wbr 4289

cxp 4834

cdm 4836

crn 4837

cres 4838

cima 4839

ccom 4840

wfun 5409

wfn 5410

wf 5411

cfv 5415 (class class class)co 6090

cmpt2 6092

cr 9277

cc0 9278

c1 9279

caddc 9281

cmul 9283

cxr 9413

clt 9414

cle 9415

cmin 9591

cdiv 9989

cn 10318

c2 10367

cn0 10575

cz 10642

crp 10987

cioo 11296

cicc 11299

cfl 11636

cexp 11861

cabs 12719

ctg 14372

cxmt 17760

cbl 17762

cmopn 17765

cvol 20906

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 1713 ax-7 1733 ax-8 1763 ax-9 1765 ax-10 1780 ax-11 1785 ax-12 1797 ax-13 1948 ax-ext 2422 ax-rep 4400 ax-sep 4410 ax-nul 4418 ax-pow 4467 ax-pr 4528 ax-un 6371 ax-inf2 7843 ax-cnex 9334 ax-resscn 9335 ax-1cn 9336 ax-icn 9337 ax-addcl 9338 ax-addrcl 9339 ax-mulcl 9340 ax-mulrcl 9341 ax-mulcom 9342 ax-addass 9343 ax-mulass 9344 ax-distr 9345 ax-i2m1 9346 ax-1ne0 9347 ax-1rid 9348 ax-rnegex 9349 ax-rrecex 9350 ax-cnre 9351 ax-pre-lttri 9352 ax-pre-lttrn 9353 ax-pre-ltadd 9354 ax-pre-mulgt0 9355 ax-pre-sup 9356

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 961 df-3an 962 df-tru 1367 df-fal 1370 df-ex 1592 df-nf 1595 df-sb 1706 df-eu 2261 df-mo 2262 df-clab 2428 df-cleq 2434 df-clel 2437 df-nfc 2566 df-ne 2606 df-nel 2607 df-ral 2718 df-rex 2719 df-reu 2720 df-rmo 2721 df-rab 2722 df-v 2972 df-sbc 3184 df-csb 3286 df-dif 3328 df-un 3330 df-in 3332 df-ss 3339 df-pss 3341 df-nul 3635 df-if 3789 df-pw 3859 df-sn 3875 df-pr 3877 df-tp 3879 df-op 3881 df-uni 4089 df-int 4126 df-iun 4170 df-disj 4260 df-br 4290 df-opab 4348 df-mpt 4349 df-tr 4383 df-eprel 4628 df-id 4632 df-po 4637 df-so 4638 df-fr 4675 df-se 4676 df-we 4677 df-ord 4718 df-on 4719 df-lim 4720 df-suc 4721 df-xp 4842 df-rel 4843 df-cnv 4844 df-co 4845 df-dm 4846 df-rn 4847 df-res 4848 df-ima 4849 df-iota 5378 df-fun 5417 df-fn 5418 df-f 5419 df-f1 5420 df-fo 5421 df-f1o 5422 df-fv 5423 df-isom 5424 df-riota 6049 df-ov 6093 df-oprab 6094 df-mpt2 6095 df-of 6319 df-om 6476 df-1st 6576 df-2nd 6577 df-recs 6828 df-rdg 6862 df-1o 6916 df-2o 6917 df-oadd 6920 df-omul 6921 df-er 7097 df-map 7212 df-pm 7213 df-en 7307 df-dom 7308 df-sdom 7309 df-fin 7310 df-fi 7657 df-sup 7687 df-oi 7720 df-card 8105 df-acn 8108 df-cda 8333 df-pnf 9416 df-mnf 9417 df-xr 9418 df-ltxr 9419 df-le 9420 df-sub 9593 df-neg 9594 df-div 9990 df-nn 10319 df-2 10376 df-3 10377 df-4 10378 df-n0 10576 df-z 10643 df-uz 10858 df-q 10950 df-rp 10988 df-xneg 11085 df-xadd 11086 df-xmul 11087 df-ioo 11300 df-ico 11302 df-icc 11303 df-fz 11434 df-fzo 11545 df-fl 11638 df-seq 11803 df-exp 11862 df-hash 12100 df-cj 12584 df-re 12585 df-im 12586 df-sqr 12720 df-abs 12721 df-clim 12962 df-rlim 12963 df-sum 13160 df-rest 14357 df-topgen 14378 df-psmet 17768 df-xmet 17769 df-met 17770 df-bl 17771 df-mopn 17772 df-top 18462 df-bases 18464 df-topon 18465 df-cmp 18949 df-ovol 20907 df-vol 20908

This theorem is referenced by: opnmbl 21041

W3C validator