ismbf3d - Metamath Proof Explorer

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

Theorem ismbf3d 21824

Description: Simplified form of ismbfd 21810. (Contributed by Mario Carneiro, 18-Jun-2014.)

**Hypotheses**
Ref	Expression
ismbf3d.1
ismbf3d.2	$/\$

**Assertion**
Ref	Expression
ismbf3d	MblFn

Distinct variable groups:

Allowed substitution hint:

(

)

Proof of Theorem ismbf3d Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ismbf3d.1	. 2
2		fimacnv 6013	. . . 4
3	1, 2	syl 16	. . 3
4		imaiun 6145	. . . . 5
5		ioossre 11586	. . . . . . . . 9
6	5	rgenw 2825	. . . . . . . 8
7		iunss 4366	. . . . . . . 8
8	6, 7	mpbir 209	. . . . . . 7
9		renegcl 9882	. . . . . . . . . . 11
10		arch 10792	. . . . . . . . . . 11
11	9, 10	syl 16	. . . . . . . . . 10
12		simpl 457	. . . . . . . . . . . . 13 $/\$
13	12	biantrurd 508	. . . . . . . . . . . 12 $/\$ $/\$
14		nnre 10543	. . . . . . . . . . . . 13
15		ltnegcon1 10053	. . . . . . . . . . . . 13 $/\$
16	14, 15	sylan2 474	. . . . . . . . . . . 12 $/\$
17	14	adantl 466	. . . . . . . . . . . . . . 15 $/\$
18	17	renegcld 9986	. . . . . . . . . . . . . 14 $/\$
19	18	rexrd 9643	. . . . . . . . . . . . 13 $/\$
20		elioopnf 11618	. . . . . . . . . . . . 13 $/\$
21	19, 20	syl 16	. . . . . . . . . . . 12 $/\$ $/\$
22	13, 16, 21	3bitr4d 285	. . . . . . . . . . 11 $/\$
23	22	rexbidva 2970	. . . . . . . . . 10
24	11, 23	mpbid 210	. . . . . . . . 9
25		eliun 4330	. . . . . . . . 9
26	24, 25	sylibr 212	. . . . . . . 8
27	26	ssriv 3508	. . . . . . 7
28	8, 27	eqssi 3520	. . . . . 6
29	28	imaeq2i 5335	. . . . 5
30	4, 29	eqtr3i 2498	. . . 4
31		ismbf3d.2	. . . . . . . 8 $/\$
32	31	ralrimiva 2878	. . . . . . 7
33	14	renegcld 9986	. . . . . . 7
34		oveq1 6291	. . . . . . . . . 10
35	34	imaeq2d 5337	. . . . . . . . 9
36	35	eleq1d 2536	. . . . . . . 8
37	36	rspccva 3213	. . . . . . 7 $/\$
38	32, 33, 37	syl2an 477	. . . . . 6 $/\$
39	38	ralrimiva 2878	. . . . 5
40		iunmbl 21726	. . . . 5
41	39, 40	syl 16	. . . 4
42	30, 41	syl5eqelr 2560	. . 3
43	3, 42	eqeltrrd 2556	. 2
44		imaiun 6145	. . . . . . 7
45		eliun 4330	. . . . . . . . . 10
46		3simpb 994	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
47		simplr 754	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
48		nnrp 11229	. . . . . . . . . . . . . . . . . . . . . 22
49	48	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
50	49	rpreccld 11266	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
51	47, 50	ltsubrpd 11284	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
52		simprr 756	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
53		simpr 461	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
54		nnrecre 10572	. . . . . . . . . . . . . . . . . . . . . 22
55		resubcl 9883	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
56	53, 54, 55	syl2an 477	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
57	56	adantrr 716	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
58		lelttr 9675	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
59	52, 57, 47, 58	syl3anc 1228	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
60	51, 59	mpan2d 674	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
61	60	anassrs 648	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
62	61	imdistanda 693	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
63	46, 62	syl5 32	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
64		mnfxr 11323	. . . . . . . . . . . . . . . 16
65		elioc2 11587	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
66	64, 56, 65	sylancr 663	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
67		rexr 9639	. . . . . . . . . . . . . . . . . 18
68	67	adantl 466	. . . . . . . . . . . . . . . . 17 $/\$
69		elioomnf 11619	. . . . . . . . . . . . . . . . 17 $/\$
70	68, 69	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
71	70	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
72	63, 66, 71	3imtr4d 268	. . . . . . . . . . . . . 14 $/\$ $/\$
73	72	rexlimdva 2955	. . . . . . . . . . . . 13 $/\$
74	73, 70	sylibd 214	. . . . . . . . . . . 12 $/\$ $/\$
75		simplr 754	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
76		simprl 755	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
77	75, 76	resubcld 9987	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
78		simprr 756	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
79	76, 75	posdifd 10139	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
80	78, 79	mpbid 210	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
81		nnrecl 10793	. . . . . . . . . . . . . . 15 $/\$
82	77, 80, 81	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
83	76	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
84		mnflt 11333	. . . . . . . . . . . . . . . . . 18
85	83, 84	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
86	56	ad2ant2r 746	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
87	54	ad2antrl 727	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
88	75	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
89		simprr 756	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
90	87, 88, 83, 89	ltsub13d 10158	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
91	83, 86, 90	ltled 9732	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
92	66	ad2ant2r 746	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
93	83, 85, 91, 92	mpbir3and 1179	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
94	93	expr 615	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
95	94	reximdva 2938	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
96	82, 95	mpd 15	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
97	96	ex 434	. . . . . . . . . . . 12 $/\$ $/\$
98	74, 97	impbid 191	. . . . . . . . . . 11 $/\$ $/\$
99	98, 70	bitr4d 256	. . . . . . . . . 10 $/\$
100	45, 99	syl5bb 257	. . . . . . . . 9 $/\$
101	100	eqrdv 2464	. . . . . . . 8 $/\$
102	101	imaeq2d 5337	. . . . . . 7 $/\$
103	44, 102	syl5eqr 2522	. . . . . 6 $/\$
104	1	ad2antrr 725	. . . . . . . . . . 11 $/\$ $/\$
105		ffun 5733	. . . . . . . . . . 11
106		funcnvcnv 5646	. . . . . . . . . . 11
107		imadif 5663	. . . . . . . . . . 11 $\$ $\$
108	104, 105, 106, 107	4syl 21	. . . . . . . . . 10 $/\$ $/\$ $\$ $\$
109	64	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
110	56	rexrd 9643	. . . . . . . . . . . . . 14 $/\$ $/\$
111		pnfxr 11321	. . . . . . . . . . . . . . 15
112	111	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
113		mnflt 11333	. . . . . . . . . . . . . . 15
114	56, 113	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$
115		ltpnf 11331	. . . . . . . . . . . . . . 15
116	56, 115	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$
117		df-ioc 11534	. . . . . . . . . . . . . . 15 $/\$
118		df-ioo 11533	. . . . . . . . . . . . . . 15 $/\$
119		xrltnle 9653	. . . . . . . . . . . . . . 15 $/\$
120		xrlelttr 11359	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
121		xrlttr 11346	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
122	117, 118, 119, 118, 120, 121	ixxun 11545	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
123	109, 110, 112, 114, 116, 122	syl32anc 1236	. . . . . . . . . . . . 13 $/\$ $/\$
124		uncom 3648	. . . . . . . . . . . . 13
125		ioomax 11599	. . . . . . . . . . . . 13
126	123, 124, 125	3eqtr3g 2531	. . . . . . . . . . . 12 $/\$ $/\$
127		ioossre 11586	. . . . . . . . . . . . 13
128		incom 3691	. . . . . . . . . . . . . 14
129	117, 118, 119	ixxdisj 11544	. . . . . . . . . . . . . . . 16 $/\$ $/\$
130	64, 111, 129	mp3an13 1315	. . . . . . . . . . . . . . 15
131	110, 130	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$
132	128, 131	syl5eq 2520	. . . . . . . . . . . . 13 $/\$ $/\$
133		uneqdifeq 3915	. . . . . . . . . . . . 13 $/\$ $\$
134	127, 132, 133	sylancr 663	. . . . . . . . . . . 12 $/\$ $/\$ $\$
135	126, 134	mpbid 210	. . . . . . . . . . 11 $/\$ $/\$ $\$
136	135	imaeq2d 5337	. . . . . . . . . 10 $/\$ $/\$ $\$
137	108, 136	eqtr3d 2510	. . . . . . . . 9 $/\$ $/\$ $\$
138	42	ad2antrr 725	. . . . . . . . . 10 $/\$ $/\$
139	32	ad2antrr 725	. . . . . . . . . . 11 $/\$ $/\$
140		oveq1 6291	. . . . . . . . . . . . . 14
141	140	imaeq2d 5337	. . . . . . . . . . . . 13
142	141	eleq1d 2536	. . . . . . . . . . . 12
143	142	rspcv 3210	. . . . . . . . . . 11
144	56, 139, 143	sylc 60	. . . . . . . . . 10 $/\$ $/\$
145		difmbl 21716	. . . . . . . . . 10 $/\$ $\$
146	138, 144, 145	syl2anc 661	. . . . . . . . 9 $/\$ $/\$ $\$
147	137, 146	eqeltrrd 2556	. . . . . . . 8 $/\$ $/\$
148	147	ralrimiva 2878	. . . . . . 7 $/\$
149		iunmbl 21726	. . . . . . 7
150	148, 149	syl 16	. . . . . 6 $/\$
151	103, 150	eqeltrrd 2556	. . . . 5 $/\$
152	151	ralrimiva 2878	. . . 4
153		oveq2 6292	. . . . . . 7
154	153	imaeq2d 5337	. . . . . 6
155	154	eleq1d 2536	. . . . 5
156	155	cbvralv 3088	. . . 4
157	152, 156	sylib 196	. . 3
158	157	r19.21bi 2833	. 2 $/\$
159	1, 43, 31, 158	ismbf2d 21811	1 MblFn

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1379

wcel 1767

wral 2814

wrex 2815 $\$ cdif 3473

cun 3474

cin 3475

wss 3476

c0 3785

ciun 4325 class class class wbr 4447

ccnv 4998

cdm 4999

cima 5002

wfun 5582

wf 5584 (class class class)co 6284

cr 9491

cc0 9492

c1 9493

cpnf 9625

cmnf 9626

cxr 9627

clt 9628

cle 9629

cmin 9805

cneg 9806

cdiv 10206

cn 10536

crp 11220

cioo 11529

cioc 11530

cvol 21638 MblFncmbf 21786

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-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6576 ax-inf2 8058 ax-cc 8815 ax-cnex 9548 ax-resscn 9549 ax-1cn 9550 ax-icn 9551 ax-addcl 9552 ax-addrcl 9553 ax-mulcl 9554 ax-mulrcl 9555 ax-mulcom 9556 ax-addass 9557 ax-mulass 9558 ax-distr 9559 ax-i2m1 9560 ax-1ne0 9561 ax-1rid 9562 ax-rnegex 9563 ax-rrecex 9564 ax-cnre 9565 ax-pre-lttri 9566 ax-pre-lttrn 9567 ax-pre-ltadd 9568 ax-pre-mulgt0 9569 ax-pre-sup 9570

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-fal 1385 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-int 4283 df-iun 4327 df-disj 4418 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-se 4839 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-isom 5597 df-riota 6245 df-ov 6287 df-oprab 6288 df-mpt2 6289 df-of 6524 df-om 6685 df-1st 6784 df-2nd 6785 df-recs 7042 df-rdg 7076 df-1o 7130 df-2o 7131 df-oadd 7134 df-er 7311 df-map 7422 df-pm 7423 df-en 7517 df-dom 7518 df-sdom 7519 df-fin 7520 df-sup 7901 df-oi 7935 df-card 8320 df-cda 8548 df-pnf 9630 df-mnf 9631 df-xr 9632 df-ltxr 9633 df-le 9634 df-sub 9807 df-neg 9808 df-div 10207 df-nn 10537 df-2 10594 df-3 10595 df-n0 10796 df-z 10865 df-uz 11083 df-q 11183 df-rp 11221 df-xadd 11319 df-ioo 11533 df-ioc 11534 df-ico 11535 df-icc 11536 df-fz 11673 df-fzo 11793 df-fl 11897 df-seq 12076 df-exp 12135 df-hash 12374 df-cj 12895 df-re 12896 df-im 12897 df-sqrt 13031 df-abs 13032 df-clim 13274 df-rlim 13275 df-sum 13472 df-xmet 18211 df-met 18212 df-ovol 21639 df-vol 21640 df-mbf 21791

This theorem is referenced by: mbfaddlem 21830 mbfsup 21834

W3C validator