opnmbllem0 - Mathbox for Brendan Leahy

	Mathbox for Brendan Leahy	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > opnmbllem0		Structured version Unicode version

Theorem opnmbllem0 28370

Description: Lemma for ismblfin 28375; could also be used to shorten proof of opnmbllem 21050. (Contributed by Brendan Leahy, 13-Jul-2018.)

**Assertion**
Ref	Expression
opnmbllem0

Distinct variable group:

Proof of Theorem opnmbllem0 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 5684	. . . . . . . 8
2	1	sseq1d 3376	. . . . . . 7
3	2	elrab 3110	. . . . . 6 $/\$
4		simprr 756	. . . . . . 7 $/\$ $/\$
5		fvex 5694	. . . . . . . 8
6	5	elpw 3859	. . . . . . 7
7	4, 6	sylibr 212	. . . . . 6 $/\$ $/\$
8	3, 7	sylan2b 475	. . . . 5 $/\$
9	8	ralrimiva 2793	. . . 4
10		iccf 11380	. . . . . 6
11		ffun 5554	. . . . . 6
12	10, 11	ax-mp 5	. . . . 5
13		ssrab2 3430	. . . . . . 7
14		oveq1 6093	. . . . . . . . . . . 12
15		oveq1 6093	. . . . . . . . . . . . 13
16	15	oveq1d 6101	. . . . . . . . . . . 12
17	14, 16	opeq12d 4060	. . . . . . . . . . 11
18		oveq2 6094	. . . . . . . . . . . . 13
19	18	oveq2d 6102	. . . . . . . . . . . 12
20	18	oveq2d 6102	. . . . . . . . . . . 12
21	19, 20	opeq12d 4060	. . . . . . . . . . 11
22	17, 21	cbvmpt2v 6161	. . . . . . . . . 10
23	22	dyadf 21040	. . . . . . . . 9
24		frn 5558	. . . . . . . . 9
25	23, 24	ax-mp 5	. . . . . . . 8
26		inss2 3564	. . . . . . . . 9
27		rexpssxrxp 9420	. . . . . . . . 9
28	26, 27	sstri 3358	. . . . . . . 8
29	25, 28	sstri 3358	. . . . . . 7
30	13, 29	sstri 3358	. . . . . 6
31	10	fdmi 5557	. . . . . 6
32	30, 31	sseqtr4i 3382	. . . . 5
33		funimass4 5735	. . . . 5 $/\$
34	12, 32, 33	mp2an 672	. . . 4
35	9, 34	sylibr 212	. . 3
36		sspwuni 4249	. . 3
37	35, 36	sylib 196	. 2
38		eqid 2437	. . . . . . 7
39	38	rexmet 20337	. . . . . 6
40		eqid 2437	. . . . . . . 8
41	38, 40	tgioo 20342	. . . . . . 7
42	41	mopni2 20037	. . . . . 6 $/\$ $/\$
43	39, 42	mp3an1 1301	. . . . 5 $/\$
44		elssuni 4114	. . . . . . . . . . 11
45		uniretop 20310	. . . . . . . . . . 11
46	44, 45	syl6sseqr 3396	. . . . . . . . . 10
47	46	sselda 3349	. . . . . . . . 9 $/\$
48		rpre 10989	. . . . . . . . 9
49	38	bl2ioo 20338	. . . . . . . . 9 $/\$
50	47, 48, 49	syl2an 477	. . . . . . . 8 $/\$ $/\$
51	50	sseq1d 3376	. . . . . . 7 $/\$ $/\$
52		2re 10383	. . . . . . . . . . 11
53		1lt2 10480	. . . . . . . . . . 11
54		expnlbnd 11986	. . . . . . . . . . 11 $/\$ $/\$
55	52, 53, 54	mp3an23 1306	. . . . . . . . . 10
56	55	ad2antrl 727	. . . . . . . . 9 $/\$ $/\$ $/\$
57	47	ad2antrr 725	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
58		2nn 10471	. . . . . . . . . . . . . . . . . 18
59		nnnn0 10578	. . . . . . . . . . . . . . . . . . 19
60	59	ad2antrl 727	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
61		nnexpcl 11870	. . . . . . . . . . . . . . . . . 18 $/\$
62	58, 60, 61	sylancr 663	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
63	62	nnred 10329	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
64	57, 63	remulcld 9406	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
65		fllelt 11639	. . . . . . . . . . . . . . 15 $/\$
66	64, 65	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
67	66	simpld 459	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
68		reflcl 11638	. . . . . . . . . . . . . . 15
69	64, 68	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
70	62	nngt0d 10357	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
71		ledivmul2 10201	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
72	69, 57, 63, 70, 71	syl112anc 1222	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
73	67, 72	mpbird 232	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
74		peano2re 9534	. . . . . . . . . . . . . . 15
75	69, 74	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
76	75, 62	nndivred 10362	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
77	66	simprd 463	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
78		ltmuldiv 10194	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
79	57, 75, 63, 70, 78	syl112anc 1222	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
80	77, 79	mpbid 210	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
81	57, 76, 80	ltled 9514	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
82	69, 62	nndivred 10362	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
83		elicc2 11352	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
84	82, 76, 83	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
85	57, 73, 81, 84	mpbir3and 1171	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
86	64	flcld 11640	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
87	22	dyadval 21041	. . . . . . . . . . . . . 14 $/\$
88	86, 60, 87	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
89	88	fveq2d 5688	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
90		df-ov 6089	. . . . . . . . . . . 12
91	89, 90	syl6eqr 2487	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
92	85, 91	eleqtrrd 2514	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
93		ffn 5552	. . . . . . . . . . . . . . 15
94	23, 93	ax-mp 5	. . . . . . . . . . . . . 14
95		fnovrn 6233	. . . . . . . . . . . . . 14 $/\$ $/\$
96	94, 95	mp3an1 1301	. . . . . . . . . . . . 13 $/\$
97	86, 60, 96	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
98		simplrl 759	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
99	98	rpred 11019	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
100	57, 99	resubcld 9768	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
101	100	rexrd 9425	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
102	57, 99	readdcld 9405	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
103	102	rexrd 9425	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
104	82, 99	readdcld 9405	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
105	69	recnd 9404	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
106		ax-1cn 9332	. . . . . . . . . . . . . . . . . . . 20
107	106	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
108	63	recnd 9404	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
109	62	nnne0d 10358	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
110	105, 107, 108, 109	divdird 10137	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
111	62	nnrecred 10359	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
112		simprr 756	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
113	111, 99, 82, 112	ltadd2dd 9522	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
114	110, 113	eqbrtrd 4305	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
115	57, 76, 104, 80, 114	lttrd 9524	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
116	57, 99, 82	ltsubaddd 9927	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
117	115, 116	mpbird 232	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
118	57, 111	readdcld 9405	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
119	82, 57, 111, 73	leadd1dd 9945	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
120	110, 119	eqbrtrd 4305	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
121	111, 99, 57, 112	ltadd2dd 9522	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
122	76, 118, 102, 120, 121	lelttrd 9521	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
123		iccssioo 11356	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
124	101, 103, 117, 122, 123	syl22anc 1219	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
125	91, 124	eqsstrd 3383	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
126		simplrr 760	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
127	125, 126	sstrd 3359	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
128		fveq2 5684	. . . . . . . . . . . . . 14
129	128	sseq1d 3376	. . . . . . . . . . . . 13
130	129	elrab 3110	. . . . . . . . . . . 12 $/\$
131	97, 127, 130	sylanbrc 664	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
132		funfvima2 5946	. . . . . . . . . . . 12 $/\$
133	12, 32, 132	mp2an 672	. . . . . . . . . . 11
134	131, 133	syl 16	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
135		elunii 4089	. . . . . . . . . 10 $/\$
136	92, 134, 135	syl2anc 661	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
137	56, 136	rexlimddv 2839	. . . . . . . 8 $/\$ $/\$ $/\$
138	137	expr 615	. . . . . . 7 $/\$ $/\$
139	51, 138	sylbid 215	. . . . . 6 $/\$ $/\$
140	139	rexlimdva 2835	. . . . 5 $/\$
141	43, 140	mpd 15	. . . 4 $/\$
142	141	ex 434	. . 3
143	142	ssrdv 3355	. 2
144	37, 143	eqssd 3366	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1369

wcel 1756

wral 2709

wrex 2710

crab 2713

cin 3320

wss 3321

cpw 3853

cop 3876

cuni 4084 class class class wbr 4285

cxp 4830

cdm 4832

crn 4833

cres 4834

cima 4835

ccom 4836

wfun 5405

wfn 5406

wf 5407

cfv 5411 (class class class)co 6086

cmpt2 6088

cc 9272

cr 9273

cc0 9274

c1 9275

caddc 9277

cmul 9279

cxr 9409

clt 9410

cle 9411

cmin 9587

cdiv 9985

cn 10314

c2 10363

cn0 10571

cz 10638

crp 10983

cioo 11292

cicc 11295

cfl 11632

cexp 11857

cabs 12715

ctg 14368

cxmt 17770

cbl 17772

cmopn 17775

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 2418 ax-sep 4406 ax-nul 4414 ax-pow 4463 ax-pr 4524 ax-un 6367 ax-cnex 9330 ax-resscn 9331 ax-1cn 9332 ax-icn 9333 ax-addcl 9334 ax-addrcl 9335 ax-mulcl 9336 ax-mulrcl 9337 ax-mulcom 9338 ax-addass 9339 ax-mulass 9340 ax-distr 9341 ax-i2m1 9342 ax-1ne0 9343 ax-1rid 9344 ax-rnegex 9345 ax-rrecex 9346 ax-cnre 9347 ax-pre-lttri 9348 ax-pre-lttrn 9349 ax-pre-ltadd 9350 ax-pre-mulgt0 9351 ax-pre-sup 9352

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2256 df-mo 2257 df-clab 2424 df-cleq 2430 df-clel 2433 df-nfc 2562 df-ne 2602 df-nel 2603 df-ral 2714 df-rex 2715 df-reu 2716 df-rmo 2717 df-rab 2718 df-v 2968 df-sbc 3180 df-csb 3282 df-dif 3324 df-un 3326 df-in 3328 df-ss 3335 df-pss 3337 df-nul 3631 df-if 3785 df-pw 3855 df-sn 3871 df-pr 3873 df-tp 3875 df-op 3877 df-uni 4085 df-iun 4166 df-br 4286 df-opab 4344 df-mpt 4345 df-tr 4379 df-eprel 4624 df-id 4628 df-po 4633 df-so 4634 df-fr 4671 df-we 4673 df-ord 4714 df-on 4715 df-lim 4716 df-suc 4717 df-xp 4838 df-rel 4839 df-cnv 4840 df-co 4841 df-dm 4842 df-rn 4843 df-res 4844 df-ima 4845 df-iota 5374 df-fun 5413 df-fn 5414 df-f 5415 df-f1 5416 df-fo 5417 df-f1o 5418 df-fv 5419 df-riota 6045 df-ov 6089 df-oprab 6090 df-mpt2 6091 df-om 6472 df-1st 6572 df-2nd 6573 df-recs 6824 df-rdg 6858 df-er 7093 df-map 7208 df-en 7303 df-dom 7304 df-sdom 7305 df-sup 7683 df-pnf 9412 df-mnf 9413 df-xr 9414 df-ltxr 9415 df-le 9416 df-sub 9589 df-neg 9590 df-div 9986 df-nn 10315 df-2 10372 df-3 10373 df-n0 10572 df-z 10639 df-uz 10854 df-q 10946 df-rp 10984 df-xneg 11081 df-xadd 11082 df-xmul 11083 df-ioo 11296 df-icc 11299 df-fl 11634 df-seq 11799 df-exp 11858 df-cj 12580 df-re 12581 df-im 12582 df-sqr 12716 df-abs 12717 df-topgen 14374 df-psmet 17778 df-xmet 17779 df-met 17780 df-bl 17781 df-mopn 17782 df-top 18472 df-bases 18474 df-topon 18475

This theorem is referenced by: mblfinlem1 28371 mblfinlem2 28372

W3C validator