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 29903

Description: Lemma for ismblfin 29908; could also be used to shorten proof of opnmbllem 21837. (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 5866	. . . . . . . 8
2	1	sseq1d 3531	. . . . . . 7
3	2	elrab 3261	. . . . . 6 $/\$
4		simprr 756	. . . . . . 7 $/\$ $/\$
5		fvex 5876	. . . . . . . 8
6	5	elpw 4016	. . . . . . 7
7	4, 6	sylibr 212	. . . . . 6 $/\$ $/\$
8	3, 7	sylan2b 475	. . . . 5 $/\$
9	8	ralrimiva 2878	. . . 4
10		iccf 11624	. . . . . 6
11		ffun 5733	. . . . . 6
12	10, 11	ax-mp 5	. . . . 5
13		ssrab2 3585	. . . . . . 7
14		oveq1 6292	. . . . . . . . . . . 12
15		oveq1 6292	. . . . . . . . . . . . 13
16	15	oveq1d 6300	. . . . . . . . . . . 12
17	14, 16	opeq12d 4221	. . . . . . . . . . 11
18		oveq2 6293	. . . . . . . . . . . . 13
19	18	oveq2d 6301	. . . . . . . . . . . 12
20	18	oveq2d 6301	. . . . . . . . . . . 12
21	19, 20	opeq12d 4221	. . . . . . . . . . 11
22	17, 21	cbvmpt2v 6362	. . . . . . . . . 10
23	22	dyadf 21827	. . . . . . . . 9
24		frn 5737	. . . . . . . . 9
25	23, 24	ax-mp 5	. . . . . . . 8
26		inss2 3719	. . . . . . . . 9
27		rexpssxrxp 9639	. . . . . . . . 9
28	26, 27	sstri 3513	. . . . . . . 8
29	25, 28	sstri 3513	. . . . . . 7
30	13, 29	sstri 3513	. . . . . 6
31	10	fdmi 5736	. . . . . 6
32	30, 31	sseqtr4i 3537	. . . . 5
33		funimass4 5919	. . . . 5 $/\$
34	12, 32, 33	mp2an 672	. . . 4
35	9, 34	sylibr 212	. . 3
36		sspwuni 4411	. . 3
37	35, 36	sylib 196	. 2
38		eqid 2467	. . . . . . 7
39	38	rexmet 21123	. . . . . 6
40		eqid 2467	. . . . . . . 8
41	38, 40	tgioo 21128	. . . . . . 7
42	41	mopni2 20823	. . . . . 6 $/\$ $/\$
43	39, 42	mp3an1 1311	. . . . 5 $/\$
44		elssuni 4275	. . . . . . . . . . 11
45		uniretop 21096	. . . . . . . . . . 11
46	44, 45	syl6sseqr 3551	. . . . . . . . . 10
47	46	sselda 3504	. . . . . . . . 9 $/\$
48		rpre 11227	. . . . . . . . 9
49	38	bl2ioo 21124	. . . . . . . . 9 $/\$
50	47, 48, 49	syl2an 477	. . . . . . . 8 $/\$ $/\$
51	50	sseq1d 3531	. . . . . . 7 $/\$ $/\$
52		2re 10606	. . . . . . . . . . 11
53		1lt2 10703	. . . . . . . . . . 11
54		expnlbnd 12265	. . . . . . . . . . 11 $/\$ $/\$
55	52, 53, 54	mp3an23 1316	. . . . . . . . . 10
56	55	ad2antrl 727	. . . . . . . . 9 $/\$ $/\$ $/\$
57	47	ad2antrr 725	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
58		2nn 10694	. . . . . . . . . . . . . . . . . 18
59		nnnn0 10803	. . . . . . . . . . . . . . . . . . 19
60	59	ad2antrl 727	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
61		nnexpcl 12148	. . . . . . . . . . . . . . . . . 18 $/\$
62	58, 60, 61	sylancr 663	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
63	62	nnred 10552	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
64	57, 63	remulcld 9625	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
65		fllelt 11903	. . . . . . . . . . . . . . 15 $/\$
66	64, 65	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
67	66	simpld 459	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
68		reflcl 11902	. . . . . . . . . . . . . . 15
69	64, 68	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
70	62	nngt0d 10580	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
71		ledivmul2 10423	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
72	69, 57, 63, 70, 71	syl112anc 1232	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
73	67, 72	mpbird 232	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
74		peano2re 9753	. . . . . . . . . . . . . . 15
75	69, 74	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
76	75, 62	nndivred 10585	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
77	66	simprd 463	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
78		ltmuldiv 10416	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
79	57, 75, 63, 70, 78	syl112anc 1232	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
80	77, 79	mpbid 210	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
81	57, 76, 80	ltled 9733	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
82	69, 62	nndivred 10585	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
83		elicc2 11590	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
84	82, 76, 83	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
85	57, 73, 81, 84	mpbir3and 1179	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
86	64	flcld 11904	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
87	22	dyadval 21828	. . . . . . . . . . . . . 14 $/\$
88	86, 60, 87	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
89	88	fveq2d 5870	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
90		df-ov 6288	. . . . . . . . . . . 12
91	89, 90	syl6eqr 2526	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
92	85, 91	eleqtrrd 2558	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
93		ffn 5731	. . . . . . . . . . . . . . 15
94	23, 93	ax-mp 5	. . . . . . . . . . . . . 14
95		fnovrn 6435	. . . . . . . . . . . . . 14 $/\$ $/\$
96	94, 95	mp3an1 1311	. . . . . . . . . . . . 13 $/\$
97	86, 60, 96	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
98		simplrl 759	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
99	98	rpred 11257	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
100	57, 99	resubcld 9988	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
101	100	rexrd 9644	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
102	57, 99	readdcld 9624	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
103	102	rexrd 9644	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
104	82, 99	readdcld 9624	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
105	69	recnd 9623	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
106		ax-1cn 9551	. . . . . . . . . . . . . . . . . . . 20
107	106	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
108	63	recnd 9623	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
109	62	nnne0d 10581	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
110	105, 107, 108, 109	divdird 10359	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
111	62	nnrecred 10582	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
112		simprr 756	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
113	111, 99, 82, 112	ltadd2dd 9741	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
114	110, 113	eqbrtrd 4467	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
115	57, 76, 104, 80, 114	lttrd 9743	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
116	57, 99, 82	ltsubaddd 10149	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
117	115, 116	mpbird 232	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
118	57, 111	readdcld 9624	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
119	82, 57, 111, 73	leadd1dd 10167	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
120	110, 119	eqbrtrd 4467	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
121	111, 99, 57, 112	ltadd2dd 9741	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
122	76, 118, 102, 120, 121	lelttrd 9740	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
123		iccssioo 11594	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
124	101, 103, 117, 122, 123	syl22anc 1229	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
125	91, 124	eqsstrd 3538	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
126		simplrr 760	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
127	125, 126	sstrd 3514	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
128		fveq2 5866	. . . . . . . . . . . . . 14
129	128	sseq1d 3531	. . . . . . . . . . . . 13
130	129	elrab 3261	. . . . . . . . . . . 12 $/\$
131	97, 127, 130	sylanbrc 664	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
132		funfvima2 6137	. . . . . . . . . . . 12 $/\$
133	12, 32, 132	mp2an 672	. . . . . . . . . . 11
134	131, 133	syl 16	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
135		elunii 4250	. . . . . . . . . 10 $/\$
136	92, 134, 135	syl2anc 661	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
137	56, 136	rexlimddv 2959	. . . . . . . 8 $/\$ $/\$ $/\$
138	137	expr 615	. . . . . . 7 $/\$ $/\$
139	51, 138	sylbid 215	. . . . . 6 $/\$ $/\$
140	139	rexlimdva 2955	. . . . 5 $/\$
141	43, 140	mpd 15	. . . 4 $/\$
142	141	ex 434	. . 3
143	142	ssrdv 3510	. 2
144	37, 143	eqssd 3521	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1379

wcel 1767

wral 2814

wrex 2815

crab 2818

cin 3475

wss 3476

cpw 4010

cop 4033

cuni 4245 class class class wbr 4447

cxp 4997

cdm 4999

crn 5000

cres 5001

cima 5002

ccom 5003

wfun 5582

wfn 5583

wf 5584

cfv 5588 (class class class)co 6285

cmpt2 6287

cc 9491

cr 9492

cc0 9493

c1 9494

caddc 9496

cmul 9498

cxr 9628

clt 9629

cle 9630

cmin 9806

cdiv 10207

cn 10537

c2 10586

cn0 10796

cz 10865

crp 11221

cioo 11530

cicc 11533

cfl 11896

cexp 12135

cabs 13033

ctg 14696

cxmt 18214

cbl 18216

cmopn 18219

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6577 ax-cnex 9549 ax-resscn 9550 ax-1cn 9551 ax-icn 9552 ax-addcl 9553 ax-addrcl 9554 ax-mulcl 9555 ax-mulrcl 9556 ax-mulcom 9557 ax-addass 9558 ax-mulass 9559 ax-distr 9560 ax-i2m1 9561 ax-1ne0 9562 ax-1rid 9563 ax-rnegex 9564 ax-rrecex 9565 ax-cnre 9566 ax-pre-lttri 9567 ax-pre-lttrn 9568 ax-pre-ltadd 9569 ax-pre-mulgt0 9570 ax-pre-sup 9571

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-iun 4327 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5551 df-fun 5590 df-fn 5591 df-f 5592 df-f1 5593 df-fo 5594 df-f1o 5595 df-fv 5596 df-riota 6246 df-ov 6288 df-oprab 6289 df-mpt2 6290 df-om 6686 df-1st 6785 df-2nd 6786 df-recs 7043 df-rdg 7077 df-er 7312 df-map 7423 df-en 7518 df-dom 7519 df-sdom 7520 df-sup 7902 df-pnf 9631 df-mnf 9632 df-xr 9633 df-ltxr 9634 df-le 9635 df-sub 9808 df-neg 9809 df-div 10208 df-nn 10538 df-2 10595 df-3 10596 df-n0 10797 df-z 10866 df-uz 11084 df-q 11184 df-rp 11222 df-xneg 11319 df-xadd 11320 df-xmul 11321 df-ioo 11534 df-icc 11537 df-fl 11898 df-seq 12077 df-exp 12136 df-cj 12898 df-re 12899 df-im 12900 df-sqrt 13034 df-abs 13035 df-topgen 14702 df-psmet 18222 df-xmet 18223 df-met 18224 df-bl 18225 df-mopn 18226 df-top 19206 df-bases 19208 df-topon 19209

This theorem is referenced by: mblfinlem1 29904 mblfinlem2 29905

W3C validator