opnmbllem - Metamath Proof Explorer

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

Theorem opnmbllem 22638

Description: Lemma for opnmbl 22639. (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 5879	. . . . . . . . 9
2	1	sseq1d 3445	. . . . . . . 8
3	2	elrab 3184	. . . . . . 7 $/\$
4		simprr 774	. . . . . . . 8 $/\$ $/\$
5		fvex 5889	. . . . . . . . 9
6	5	elpw 3948	. . . . . . . 8
7	4, 6	sylibr 217	. . . . . . 7 $/\$ $/\$
8	3, 7	sylan2b 483	. . . . . 6 $/\$
9	8	ralrimiva 2809	. . . . 5
10		iccf 11758	. . . . . . 7
11		ffun 5742	. . . . . . 7
12	10, 11	ax-mp 5	. . . . . 6
13		ssrab2 3500	. . . . . . . 8
14		dyadmbl.1	. . . . . . . . . . 11
15	14	dyadf 22628	. . . . . . . . . 10
16		frn 5747	. . . . . . . . . 10
17	15, 16	ax-mp 5	. . . . . . . . 9
18		inss2 3644	. . . . . . . . . 10
19		rexpssxrxp 9703	. . . . . . . . . 10
20	18, 19	sstri 3427	. . . . . . . . 9
21	17, 20	sstri 3427	. . . . . . . 8
22	13, 21	sstri 3427	. . . . . . 7
23	10	fdmi 5746	. . . . . . 7
24	22, 23	sseqtr4i 3451	. . . . . 6
25		funimass4 5930	. . . . . 6 $/\$
26	12, 24, 25	mp2an 686	. . . . 5
27	9, 26	sylibr 217	. . . 4
28		sspwuni 4360	. . . 4
29	27, 28	sylib 201	. . 3
30		eqid 2471	. . . . . . . 8
31	30	rexmet 21887	. . . . . . 7
32		eqid 2471	. . . . . . . . 9
33	30, 32	tgioo 21892	. . . . . . . 8
34	33	mopni2 21586	. . . . . . 7 $/\$ $/\$
35	31, 34	mp3an1 1377	. . . . . 6 $/\$
36		elssuni 4219	. . . . . . . . . . . 12
37		uniretop 21861	. . . . . . . . . . . 12
38	36, 37	syl6sseqr 3465	. . . . . . . . . . 11
39	38	sselda 3418	. . . . . . . . . 10 $/\$
40		rpre 11331	. . . . . . . . . 10
41	30	bl2ioo 21888	. . . . . . . . . 10 $/\$
42	39, 40, 41	syl2an 485	. . . . . . . . 9 $/\$ $/\$
43	42	sseq1d 3445	. . . . . . . 8 $/\$ $/\$
44		2re 10701	. . . . . . . . . . . 12
45		1lt2 10799	. . . . . . . . . . . 12
46		expnlbnd 12440	. . . . . . . . . . . 12 $/\$ $/\$
47	44, 45, 46	mp3an23 1382	. . . . . . . . . . 11
48	47	ad2antrl 742	. . . . . . . . . 10 $/\$ $/\$ $/\$
49	39	ad2antrr 740	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
50		2nn 10790	. . . . . . . . . . . . . . . . . . 19
51		nnnn0 10900	. . . . . . . . . . . . . . . . . . . 20
52	51	ad2antrl 742	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
53		nnexpcl 12323	. . . . . . . . . . . . . . . . . . 19 $/\$
54	50, 52, 53	sylancr 676	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
55	54	nnred 10646	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
56	49, 55	remulcld 9689	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
57		fllelt 12066	. . . . . . . . . . . . . . . 16 $/\$
58	56, 57	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59	58	simpld 466	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
60		reflcl 12065	. . . . . . . . . . . . . . . 16
61	56, 60	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
62	54	nngt0d 10675	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
63		ledivmul2 10506	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
64	61, 49, 55, 62, 63	syl112anc 1296	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
65	59, 64	mpbird 240	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
66		peano2re 9824	. . . . . . . . . . . . . . . 16
67	61, 66	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
68	67, 54	nndivred 10680	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
69	58	simprd 470	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
70		ltmuldiv 10500	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
71	49, 67, 55, 62, 70	syl112anc 1296	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
72	69, 71	mpbid 215	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
73	49, 68, 72	ltled 9800	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
74	61, 54	nndivred 10680	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
75		elicc2 11724	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
76	74, 68, 75	syl2anc 673	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
77	49, 65, 73, 76	mpbir3and 1213	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
78	56	flcld 12067	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
79	14	dyadval 22629	. . . . . . . . . . . . . . 15 $/\$
80	78, 52, 79	syl2anc 673	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
81	80	fveq2d 5883	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
82		df-ov 6311	. . . . . . . . . . . . 13
83	81, 82	syl6eqr 2523	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
84	77, 83	eleqtrrd 2552	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
85		ffn 5739	. . . . . . . . . . . . . . . 16
86	15, 85	ax-mp 5	. . . . . . . . . . . . . . 15
87		fnovrn 6463	. . . . . . . . . . . . . . 15 $/\$ $/\$
88	86, 87	mp3an1 1377	. . . . . . . . . . . . . 14 $/\$
89	78, 52, 88	syl2anc 673	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
90		simplrl 778	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
91	90	rpred 11364	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
92	49, 91	resubcld 10068	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
93	92	rexrd 9708	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
94	49, 91	readdcld 9688	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
95	94	rexrd 9708	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
96	74, 91	readdcld 9688	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
97	61	recnd 9687	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
98		1cnd 9677	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
99	55	recnd 9687	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
100	54	nnne0d 10676	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
101	97, 98, 99, 100	divdird 10443	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
102	54	nnrecred 10677	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
103		simprr 774	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
104	102, 91, 74, 103	ltadd2dd 9811	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
105	101, 104	eqbrtrd 4416	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
106	49, 68, 96, 72, 105	lttrd 9813	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
107	49, 91, 74	ltsubaddd 10230	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
108	106, 107	mpbird 240	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
109	49, 102	readdcld 9688	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
110	74, 49, 102, 65	leadd1dd 10248	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
111	101, 110	eqbrtrd 4416	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
112	102, 91, 49, 103	ltadd2dd 9811	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
113	68, 109, 94, 111, 112	lelttrd 9810	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
114		iccssioo 11728	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
115	93, 95, 108, 113, 114	syl22anc 1293	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
116	83, 115	eqsstrd 3452	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
117		simplrr 779	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
118	116, 117	sstrd 3428	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
119		fveq2 5879	. . . . . . . . . . . . . . 15
120	119	sseq1d 3445	. . . . . . . . . . . . . 14
121	120	elrab 3184	. . . . . . . . . . . . 13 $/\$
122	89, 118, 121	sylanbrc 677	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
123		funfvima2 6158	. . . . . . . . . . . . 13 $/\$
124	12, 24, 123	mp2an 686	. . . . . . . . . . . 12
125	122, 124	syl 17	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
126		elunii 4195	. . . . . . . . . . 11 $/\$
127	84, 125, 126	syl2anc 673	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
128	48, 127	rexlimddv 2875	. . . . . . . . 9 $/\$ $/\$ $/\$
129	128	expr 626	. . . . . . . 8 $/\$ $/\$
130	43, 129	sylbid 223	. . . . . . 7 $/\$ $/\$
131	130	rexlimdva 2871	. . . . . 6 $/\$
132	35, 131	mpd 15	. . . . 5 $/\$
133	132	ex 441	. . . 4
134	133	ssrdv 3424	. . 3
135	29, 134	eqssd 3435	. 2
136		fveq2 5879	. . . . . . 7
137	136	sseq1d 3445	. . . . . 6
138		equequ1 1875	. . . . . 6
139	137, 138	imbi12d 327	. . . . 5
140	139	ralbidv 2829	. . . 4
141	140	cbvrabv 3030	. . 3
142	13	a1i 11	. . 3
143	14, 141, 142	dyadmbl 22637	. 2
144	135, 143	eqeltrrd 2550	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 189 $/\$ wa 376 $/\$ w3a 1007

wceq 1452

wcel 1904

wral 2756

wrex 2757

crab 2760

cin 3389

wss 3390

cpw 3942

cop 3965

cuni 4190 class class class wbr 4395

cxp 4837

cdm 4839

crn 4840

cres 4841

cima 4842

ccom 4843

wfun 5583

wfn 5584

wf 5585

cfv 5589 (class class class)co 6308

cmpt2 6310

cr 9556

cc0 9557

c1 9558

caddc 9560

cmul 9562

cxr 9692

clt 9693

cle 9694

cmin 9880

cdiv 10291

cn 10631

c2 10681

cn0 10893

cz 10961

crp 11325

cioo 11660

cicc 11663

cfl 12059

cexp 12310

cabs 13374

ctg 15414

cxmt 19032

cbl 19034

cmopn 19037

cvol 22493

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-inf2 8164 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-fal 1458 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-disj 4367 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-se 4799 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-isom 5598 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-of 6550 df-om 6712 df-1st 6812 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-2o 7201 df-oadd 7204 df-omul 7205 df-er 7381 df-map 7492 df-pm 7493 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-fi 7943 df-sup 7974 df-inf 7975 df-oi 8043 df-card 8391 df-acn 8394 df-cda 8616 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-nn 10632 df-2 10690 df-3 10691 df-4 10692 df-n0 10894 df-z 10962 df-uz 11183 df-q 11288 df-rp 11326 df-xneg 11432 df-xadd 11433 df-xmul 11434 df-ioo 11664 df-ico 11666 df-icc 11667 df-fz 11811 df-fzo 11943 df-fl 12061 df-seq 12252 df-exp 12311 df-hash 12554 df-cj 13239 df-re 13240 df-im 13241 df-sqrt 13375 df-abs 13376 df-clim 13629 df-rlim 13630 df-sum 13830 df-rest 15399 df-topgen 15420 df-psmet 19039 df-xmet 19040 df-met 19041 df-bl 19042 df-mopn 19043 df-top 19998 df-bases 19999 df-topon 20000 df-cmp 20479 df-ovol 22494 df-vol 22496

This theorem is referenced by: opnmbl 22639

W3C validator