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 28453

Description: Lemma for ismblfin 28458; could also be used to shorten proof of opnmbllem 21103. (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 5712	. . . . . . . 8
2	1	sseq1d 3404	. . . . . . 7
3	2	elrab 3138	. . . . . 6 $/\$
4		simprr 756	. . . . . . 7 $/\$ $/\$
5		fvex 5722	. . . . . . . 8
6	5	elpw 3887	. . . . . . 7
7	4, 6	sylibr 212	. . . . . 6 $/\$ $/\$
8	3, 7	sylan2b 475	. . . . 5 $/\$
9	8	ralrimiva 2820	. . . 4
10		iccf 11409	. . . . . 6
11		ffun 5582	. . . . . 6
12	10, 11	ax-mp 5	. . . . 5
13		ssrab2 3458	. . . . . . 7
14		oveq1 6119	. . . . . . . . . . . 12
15		oveq1 6119	. . . . . . . . . . . . 13
16	15	oveq1d 6127	. . . . . . . . . . . 12
17	14, 16	opeq12d 4088	. . . . . . . . . . 11
18		oveq2 6120	. . . . . . . . . . . . 13
19	18	oveq2d 6128	. . . . . . . . . . . 12
20	18	oveq2d 6128	. . . . . . . . . . . 12
21	19, 20	opeq12d 4088	. . . . . . . . . . 11
22	17, 21	cbvmpt2v 6187	. . . . . . . . . 10
23	22	dyadf 21093	. . . . . . . . 9
24		frn 5586	. . . . . . . . 9
25	23, 24	ax-mp 5	. . . . . . . 8
26		inss2 3592	. . . . . . . . 9
27		rexpssxrxp 9449	. . . . . . . . 9
28	26, 27	sstri 3386	. . . . . . . 8
29	25, 28	sstri 3386	. . . . . . 7
30	13, 29	sstri 3386	. . . . . 6
31	10	fdmi 5585	. . . . . 6
32	30, 31	sseqtr4i 3410	. . . . 5
33		funimass4 5763	. . . . 5 $/\$
34	12, 32, 33	mp2an 672	. . . 4
35	9, 34	sylibr 212	. . 3
36		sspwuni 4277	. . 3
37	35, 36	sylib 196	. 2
38		eqid 2443	. . . . . . 7
39	38	rexmet 20390	. . . . . 6
40		eqid 2443	. . . . . . . 8
41	38, 40	tgioo 20395	. . . . . . 7
42	41	mopni2 20090	. . . . . 6 $/\$ $/\$
43	39, 42	mp3an1 1301	. . . . 5 $/\$
44		elssuni 4142	. . . . . . . . . . 11
45		uniretop 20363	. . . . . . . . . . 11
46	44, 45	syl6sseqr 3424	. . . . . . . . . 10
47	46	sselda 3377	. . . . . . . . 9 $/\$
48		rpre 11018	. . . . . . . . 9
49	38	bl2ioo 20391	. . . . . . . . 9 $/\$
50	47, 48, 49	syl2an 477	. . . . . . . 8 $/\$ $/\$
51	50	sseq1d 3404	. . . . . . 7 $/\$ $/\$
52		2re 10412	. . . . . . . . . . 11
53		1lt2 10509	. . . . . . . . . . 11
54		expnlbnd 12015	. . . . . . . . . . 11 $/\$ $/\$
55	52, 53, 54	mp3an23 1306	. . . . . . . . . 10
56	55	ad2antrl 727	. . . . . . . . 9 $/\$ $/\$ $/\$
57	47	ad2antrr 725	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
58		2nn 10500	. . . . . . . . . . . . . . . . . 18
59		nnnn0 10607	. . . . . . . . . . . . . . . . . . 19
60	59	ad2antrl 727	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
61		nnexpcl 11899	. . . . . . . . . . . . . . . . . 18 $/\$
62	58, 60, 61	sylancr 663	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
63	62	nnred 10358	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
64	57, 63	remulcld 9435	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
65		fllelt 11668	. . . . . . . . . . . . . . 15 $/\$
66	64, 65	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
67	66	simpld 459	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
68		reflcl 11667	. . . . . . . . . . . . . . 15
69	64, 68	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
70	62	nngt0d 10386	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
71		ledivmul2 10230	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
72	69, 57, 63, 70, 71	syl112anc 1222	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
73	67, 72	mpbird 232	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
74		peano2re 9563	. . . . . . . . . . . . . . 15
75	69, 74	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
76	75, 62	nndivred 10391	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
77	66	simprd 463	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
78		ltmuldiv 10223	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
79	57, 75, 63, 70, 78	syl112anc 1222	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
80	77, 79	mpbid 210	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
81	57, 76, 80	ltled 9543	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
82	69, 62	nndivred 10391	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
83		elicc2 11381	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
84	82, 76, 83	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
85	57, 73, 81, 84	mpbir3and 1171	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
86	64	flcld 11669	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
87	22	dyadval 21094	. . . . . . . . . . . . . 14 $/\$
88	86, 60, 87	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
89	88	fveq2d 5716	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
90		df-ov 6115	. . . . . . . . . . . 12
91	89, 90	syl6eqr 2493	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
92	85, 91	eleqtrrd 2520	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
93		ffn 5580	. . . . . . . . . . . . . . 15
94	23, 93	ax-mp 5	. . . . . . . . . . . . . 14
95		fnovrn 6259	. . . . . . . . . . . . . 14 $/\$ $/\$
96	94, 95	mp3an1 1301	. . . . . . . . . . . . 13 $/\$
97	86, 60, 96	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
98		simplrl 759	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
99	98	rpred 11048	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
100	57, 99	resubcld 9797	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
101	100	rexrd 9454	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
102	57, 99	readdcld 9434	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
103	102	rexrd 9454	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
104	82, 99	readdcld 9434	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
105	69	recnd 9433	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
106		ax-1cn 9361	. . . . . . . . . . . . . . . . . . . 20
107	106	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
108	63	recnd 9433	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
109	62	nnne0d 10387	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
110	105, 107, 108, 109	divdird 10166	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
111	62	nnrecred 10388	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
112		simprr 756	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
113	111, 99, 82, 112	ltadd2dd 9551	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
114	110, 113	eqbrtrd 4333	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
115	57, 76, 104, 80, 114	lttrd 9553	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
116	57, 99, 82	ltsubaddd 9956	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
117	115, 116	mpbird 232	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
118	57, 111	readdcld 9434	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
119	82, 57, 111, 73	leadd1dd 9974	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
120	110, 119	eqbrtrd 4333	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
121	111, 99, 57, 112	ltadd2dd 9551	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
122	76, 118, 102, 120, 121	lelttrd 9550	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
123		iccssioo 11385	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
124	101, 103, 117, 122, 123	syl22anc 1219	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
125	91, 124	eqsstrd 3411	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
126		simplrr 760	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
127	125, 126	sstrd 3387	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
128		fveq2 5712	. . . . . . . . . . . . . 14
129	128	sseq1d 3404	. . . . . . . . . . . . 13
130	129	elrab 3138	. . . . . . . . . . . 12 $/\$
131	97, 127, 130	sylanbrc 664	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
132		funfvima2 5974	. . . . . . . . . . . 12 $/\$
133	12, 32, 132	mp2an 672	. . . . . . . . . . 11
134	131, 133	syl 16	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
135		elunii 4117	. . . . . . . . . 10 $/\$
136	92, 134, 135	syl2anc 661	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
137	56, 136	rexlimddv 2866	. . . . . . . 8 $/\$ $/\$ $/\$
138	137	expr 615	. . . . . . 7 $/\$ $/\$
139	51, 138	sylbid 215	. . . . . 6 $/\$ $/\$
140	139	rexlimdva 2862	. . . . 5 $/\$
141	43, 140	mpd 15	. . . 4 $/\$
142	141	ex 434	. . 3
143	142	ssrdv 3383	. 2
144	37, 143	eqssd 3394	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1369

wcel 1756

wral 2736

wrex 2737

crab 2740

cin 3348

wss 3349

cpw 3881

cop 3904

cuni 4112 class class class wbr 4313

cxp 4859

cdm 4861

crn 4862

cres 4863

cima 4864

ccom 4865

wfun 5433

wfn 5434

wf 5435

cfv 5439 (class class class)co 6112

cmpt2 6114

cc 9301

cr 9302

cc0 9303

c1 9304

caddc 9306

cmul 9308

cxr 9438

clt 9439

cle 9440

cmin 9616

cdiv 10014

cn 10343

c2 10392

cn0 10600

cz 10667

crp 11012

cioo 11321

cicc 11324

cfl 11661

cexp 11886

cabs 12744

ctg 14397

cxmt 17823

cbl 17825

cmopn 17828

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-sep 4434 ax-nul 4442 ax-pow 4491 ax-pr 4552 ax-un 6393 ax-cnex 9359 ax-resscn 9360 ax-1cn 9361 ax-icn 9362 ax-addcl 9363 ax-addrcl 9364 ax-mulcl 9365 ax-mulrcl 9366 ax-mulcom 9367 ax-addass 9368 ax-mulass 9369 ax-distr 9370 ax-i2m1 9371 ax-1ne0 9372 ax-1rid 9373 ax-rnegex 9374 ax-rrecex 9375 ax-cnre 9376 ax-pre-lttri 9377 ax-pre-lttrn 9378 ax-pre-ltadd 9379 ax-pre-mulgt0 9380 ax-pre-sup 9381

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 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2577 df-ne 2622 df-nel 2623 df-ral 2741 df-rex 2742 df-reu 2743 df-rmo 2744 df-rab 2745 df-v 2995 df-sbc 3208 df-csb 3310 df-dif 3352 df-un 3354 df-in 3356 df-ss 3363 df-pss 3365 df-nul 3659 df-if 3813 df-pw 3883 df-sn 3899 df-pr 3901 df-tp 3903 df-op 3905 df-uni 4113 df-iun 4194 df-br 4314 df-opab 4372 df-mpt 4373 df-tr 4407 df-eprel 4653 df-id 4657 df-po 4662 df-so 4663 df-fr 4700 df-we 4702 df-ord 4743 df-on 4744 df-lim 4745 df-suc 4746 df-xp 4867 df-rel 4868 df-cnv 4869 df-co 4870 df-dm 4871 df-rn 4872 df-res 4873 df-ima 4874 df-iota 5402 df-fun 5441 df-fn 5442 df-f 5443 df-f1 5444 df-fo 5445 df-f1o 5446 df-fv 5447 df-riota 6073 df-ov 6115 df-oprab 6116 df-mpt2 6117 df-om 6498 df-1st 6598 df-2nd 6599 df-recs 6853 df-rdg 6887 df-er 7122 df-map 7237 df-en 7332 df-dom 7333 df-sdom 7334 df-sup 7712 df-pnf 9441 df-mnf 9442 df-xr 9443 df-ltxr 9444 df-le 9445 df-sub 9618 df-neg 9619 df-div 10015 df-nn 10344 df-2 10401 df-3 10402 df-n0 10601 df-z 10668 df-uz 10883 df-q 10975 df-rp 11013 df-xneg 11110 df-xadd 11111 df-xmul 11112 df-ioo 11325 df-icc 11328 df-fl 11663 df-seq 11828 df-exp 11887 df-cj 12609 df-re 12610 df-im 12611 df-sqr 12745 df-abs 12746 df-topgen 14403 df-psmet 17831 df-xmet 17832 df-met 17833 df-bl 17834 df-mopn 17835 df-top 18525 df-bases 18527 df-topon 18528

This theorem is referenced by: mblfinlem1 28454 mblfinlem2 28455

W3C validator