opnmbllem - Metamath Proof Explorer

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

Theorem opnmbllem 21096

Description: Lemma for opnmbl 21097. (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 5706	. . . . . . . . 9
2	1	sseq1d 3398	. . . . . . . 8
3	2	elrab 3132	. . . . . . 7 $/\$
4		simprr 756	. . . . . . . 8 $/\$ $/\$
5		fvex 5716	. . . . . . . . 9
6	5	elpw 3881	. . . . . . . 8
7	4, 6	sylibr 212	. . . . . . 7 $/\$ $/\$
8	3, 7	sylan2b 475	. . . . . 6 $/\$
9	8	ralrimiva 2814	. . . . 5
10		iccf 11403	. . . . . . 7
11		ffun 5576	. . . . . . 7
12	10, 11	ax-mp 5	. . . . . 6
13		ssrab2 3452	. . . . . . . 8
14		dyadmbl.1	. . . . . . . . . . 11
15	14	dyadf 21086	. . . . . . . . . 10
16		frn 5580	. . . . . . . . . 10
17	15, 16	ax-mp 5	. . . . . . . . 9
18		inss2 3586	. . . . . . . . . 10
19		rexpssxrxp 9443	. . . . . . . . . 10
20	18, 19	sstri 3380	. . . . . . . . 9
21	17, 20	sstri 3380	. . . . . . . 8
22	13, 21	sstri 3380	. . . . . . 7
23	10	fdmi 5579	. . . . . . 7
24	22, 23	sseqtr4i 3404	. . . . . 6
25		funimass4 5757	. . . . . 6 $/\$
26	12, 24, 25	mp2an 672	. . . . 5
27	9, 26	sylibr 212	. . . 4
28		sspwuni 4271	. . . 4
29	27, 28	sylib 196	. . 3
30		eqid 2443	. . . . . . . 8
31	30	rexmet 20383	. . . . . . 7
32		eqid 2443	. . . . . . . . 9
33	30, 32	tgioo 20388	. . . . . . . 8
34	33	mopni2 20083	. . . . . . 7 $/\$ $/\$
35	31, 34	mp3an1 1301	. . . . . 6 $/\$
36		elssuni 4136	. . . . . . . . . . . 12
37		uniretop 20356	. . . . . . . . . . . 12
38	36, 37	syl6sseqr 3418	. . . . . . . . . . 11
39	38	sselda 3371	. . . . . . . . . 10 $/\$
40		rpre 11012	. . . . . . . . . 10
41	30	bl2ioo 20384	. . . . . . . . . 10 $/\$
42	39, 40, 41	syl2an 477	. . . . . . . . 9 $/\$ $/\$
43	42	sseq1d 3398	. . . . . . . 8 $/\$ $/\$
44		2re 10406	. . . . . . . . . . . 12
45		1lt2 10503	. . . . . . . . . . . 12
46		expnlbnd 12009	. . . . . . . . . . . 12 $/\$ $/\$
47	44, 45, 46	mp3an23 1306	. . . . . . . . . . 11
48	47	ad2antrl 727	. . . . . . . . . 10 $/\$ $/\$ $/\$
49	39	ad2antrr 725	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
50		2nn 10494	. . . . . . . . . . . . . . . . . . 19
51		nnnn0 10601	. . . . . . . . . . . . . . . . . . . 20
52	51	ad2antrl 727	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
53		nnexpcl 11893	. . . . . . . . . . . . . . . . . . 19 $/\$
54	50, 52, 53	sylancr 663	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
55	54	nnred 10352	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
56	49, 55	remulcld 9429	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
57		fllelt 11662	. . . . . . . . . . . . . . . 16 $/\$
58	56, 57	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59	58	simpld 459	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
60		reflcl 11661	. . . . . . . . . . . . . . . 16
61	56, 60	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
62	54	nngt0d 10380	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
63		ledivmul2 10224	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
64	61, 49, 55, 62, 63	syl112anc 1222	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
65	59, 64	mpbird 232	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
66		peano2re 9557	. . . . . . . . . . . . . . . 16
67	61, 66	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
68	67, 54	nndivred 10385	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
69	58	simprd 463	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
70		ltmuldiv 10217	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
71	49, 67, 55, 62, 70	syl112anc 1222	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
72	69, 71	mpbid 210	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
73	49, 68, 72	ltled 9537	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
74	61, 54	nndivred 10385	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
75		elicc2 11375	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
76	74, 68, 75	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
77	49, 65, 73, 76	mpbir3and 1171	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
78	56	flcld 11663	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
79	14	dyadval 21087	. . . . . . . . . . . . . . 15 $/\$
80	78, 52, 79	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
81	80	fveq2d 5710	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
82		df-ov 6109	. . . . . . . . . . . . 13
83	81, 82	syl6eqr 2493	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
84	77, 83	eleqtrrd 2520	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
85		ffn 5574	. . . . . . . . . . . . . . . 16
86	15, 85	ax-mp 5	. . . . . . . . . . . . . . 15
87		fnovrn 6253	. . . . . . . . . . . . . . 15 $/\$ $/\$
88	86, 87	mp3an1 1301	. . . . . . . . . . . . . 14 $/\$
89	78, 52, 88	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
90		simplrl 759	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
91	90	rpred 11042	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
92	49, 91	resubcld 9791	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
93	92	rexrd 9448	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
94	49, 91	readdcld 9428	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
95	94	rexrd 9448	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
96	74, 91	readdcld 9428	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
97	61	recnd 9427	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
98		1cnd 9417	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
99	55	recnd 9427	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
100	54	nnne0d 10381	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
101	97, 98, 99, 100	divdird 10160	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
102	54	nnrecred 10382	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
103		simprr 756	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
104	102, 91, 74, 103	ltadd2dd 9545	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
105	101, 104	eqbrtrd 4327	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
106	49, 68, 96, 72, 105	lttrd 9547	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
107	49, 91, 74	ltsubaddd 9950	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
108	106, 107	mpbird 232	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
109	49, 102	readdcld 9428	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
110	74, 49, 102, 65	leadd1dd 9968	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
111	101, 110	eqbrtrd 4327	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
112	102, 91, 49, 103	ltadd2dd 9545	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
113	68, 109, 94, 111, 112	lelttrd 9544	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
114		iccssioo 11379	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
115	93, 95, 108, 113, 114	syl22anc 1219	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
116	83, 115	eqsstrd 3405	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
117		simplrr 760	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
118	116, 117	sstrd 3381	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
119		fveq2 5706	. . . . . . . . . . . . . . 15
120	119	sseq1d 3398	. . . . . . . . . . . . . 14
121	120	elrab 3132	. . . . . . . . . . . . 13 $/\$
122	89, 118, 121	sylanbrc 664	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
123		funfvima2 5968	. . . . . . . . . . . . 13 $/\$
124	12, 24, 123	mp2an 672	. . . . . . . . . . . 12
125	122, 124	syl 16	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
126		elunii 4111	. . . . . . . . . . 11 $/\$
127	84, 125, 126	syl2anc 661	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
128	48, 127	rexlimddv 2860	. . . . . . . . 9 $/\$ $/\$ $/\$
129	128	expr 615	. . . . . . . 8 $/\$ $/\$
130	43, 129	sylbid 215	. . . . . . 7 $/\$ $/\$
131	130	rexlimdva 2856	. . . . . 6 $/\$
132	35, 131	mpd 15	. . . . 5 $/\$
133	132	ex 434	. . . 4
134	133	ssrdv 3377	. . 3
135	29, 134	eqssd 3388	. 2
136		fveq2 5706	. . . . . . 7
137	136	sseq1d 3398	. . . . . 6
138		equequ1 1736	. . . . . 6
139	137, 138	imbi12d 320	. . . . 5
140	139	ralbidv 2750	. . . 4
141	140	cbvrabv 2986	. . 3
142	13	a1i 11	. . 3
143	14, 141, 142	dyadmbl 21095	. 2
144	135, 143	eqeltrrd 2518	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1369

wcel 1756

wral 2730

wrex 2731

crab 2734

cin 3342

wss 3343

cpw 3875

cop 3898

cuni 4106 class class class wbr 4307

cxp 4853

cdm 4855

crn 4856

cres 4857

cima 4858

ccom 4859

wfun 5427

wfn 5428

wf 5429

cfv 5433 (class class class)co 6106

cmpt2 6108

cr 9296

cc0 9297

c1 9298

caddc 9300

cmul 9302

cxr 9432

clt 9433

cle 9434

cmin 9610

cdiv 10008

cn 10337

c2 10386

cn0 10594

cz 10661

crp 11006

cioo 11315

cicc 11318

cfl 11655

cexp 11880

cabs 12738

ctg 14391

cxmt 17816

cbl 17818

cmopn 17821

cvol 20962

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-rep 4418 ax-sep 4428 ax-nul 4436 ax-pow 4485 ax-pr 4546 ax-un 6387 ax-inf2 7862 ax-cnex 9353 ax-resscn 9354 ax-1cn 9355 ax-icn 9356 ax-addcl 9357 ax-addrcl 9358 ax-mulcl 9359 ax-mulrcl 9360 ax-mulcom 9361 ax-addass 9362 ax-mulass 9363 ax-distr 9364 ax-i2m1 9365 ax-1ne0 9366 ax-1rid 9367 ax-rnegex 9368 ax-rrecex 9369 ax-cnre 9370 ax-pre-lttri 9371 ax-pre-lttrn 9372 ax-pre-ltadd 9373 ax-pre-mulgt0 9374 ax-pre-sup 9375

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-fal 1375 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2577 df-ne 2622 df-nel 2623 df-ral 2735 df-rex 2736 df-reu 2737 df-rmo 2738 df-rab 2739 df-v 2989 df-sbc 3202 df-csb 3304 df-dif 3346 df-un 3348 df-in 3350 df-ss 3357 df-pss 3359 df-nul 3653 df-if 3807 df-pw 3877 df-sn 3893 df-pr 3895 df-tp 3897 df-op 3899 df-uni 4107 df-int 4144 df-iun 4188 df-disj 4278 df-br 4308 df-opab 4366 df-mpt 4367 df-tr 4401 df-eprel 4647 df-id 4651 df-po 4656 df-so 4657 df-fr 4694 df-se 4695 df-we 4696 df-ord 4737 df-on 4738 df-lim 4739 df-suc 4740 df-xp 4861 df-rel 4862 df-cnv 4863 df-co 4864 df-dm 4865 df-rn 4866 df-res 4867 df-ima 4868 df-iota 5396 df-fun 5435 df-fn 5436 df-f 5437 df-f1 5438 df-fo 5439 df-f1o 5440 df-fv 5441 df-isom 5442 df-riota 6067 df-ov 6109 df-oprab 6110 df-mpt2 6111 df-of 6335 df-om 6492 df-1st 6592 df-2nd 6593 df-recs 6847 df-rdg 6881 df-1o 6935 df-2o 6936 df-oadd 6939 df-omul 6940 df-er 7116 df-map 7231 df-pm 7232 df-en 7326 df-dom 7327 df-sdom 7328 df-fin 7329 df-fi 7676 df-sup 7706 df-oi 7739 df-card 8124 df-acn 8127 df-cda 8352 df-pnf 9435 df-mnf 9436 df-xr 9437 df-ltxr 9438 df-le 9439 df-sub 9612 df-neg 9613 df-div 10009 df-nn 10338 df-2 10395 df-3 10396 df-4 10397 df-n0 10595 df-z 10662 df-uz 10877 df-q 10969 df-rp 11007 df-xneg 11104 df-xadd 11105 df-xmul 11106 df-ioo 11319 df-ico 11321 df-icc 11322 df-fz 11453 df-fzo 11564 df-fl 11657 df-seq 11822 df-exp 11881 df-hash 12119 df-cj 12603 df-re 12604 df-im 12605 df-sqr 12739 df-abs 12740 df-clim 12981 df-rlim 12982 df-sum 13179 df-rest 14376 df-topgen 14397 df-psmet 17824 df-xmet 17825 df-met 17826 df-bl 17827 df-mopn 17828 df-top 18518 df-bases 18520 df-topon 18521 df-cmp 19005 df-ovol 20963 df-vol 20964

This theorem is referenced by: opnmbl 21097

W3C validator