ismbf3d - Metamath Proof Explorer

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

Theorem ismbf3d 21132

Description: Simplified form of ismbfd 21118. (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 5835	. . . 4
3	1, 2	syl 16	. . 3
4		imaiun 5962	. . . . 5
5		ioossre 11357	. . . . . . . . 9
6	5	rgenw 2783	. . . . . . . 8
7		iunss 4211	. . . . . . . 8
8	6, 7	mpbir 209	. . . . . . 7
9		renegcl 9672	. . . . . . . . . . 11
10		arch 10576	. . . . . . . . . . 11
11	9, 10	syl 16	. . . . . . . . . 10
12		simpl 457	. . . . . . . . . . . . 13 $/\$
13	12	biantrurd 508	. . . . . . . . . . . 12 $/\$ $/\$
14		nnre 10329	. . . . . . . . . . . . 13
15		ltnegcon1 9840	. . . . . . . . . . . . 13 $/\$
16	14, 15	sylan2 474	. . . . . . . . . . . 12 $/\$
17	14	adantl 466	. . . . . . . . . . . . . . 15 $/\$
18	17	renegcld 9775	. . . . . . . . . . . . . 14 $/\$
19	18	rexrd 9433	. . . . . . . . . . . . 13 $/\$
20		elioopnf 11383	. . . . . . . . . . . . 13 $/\$
21	19, 20	syl 16	. . . . . . . . . . . 12 $/\$ $/\$
22	13, 16, 21	3bitr4d 285	. . . . . . . . . . 11 $/\$
23	22	rexbidva 2732	. . . . . . . . . 10
24	11, 23	mpbid 210	. . . . . . . . 9
25		eliun 4175	. . . . . . . . 9
26	24, 25	sylibr 212	. . . . . . . 8
27	26	ssriv 3360	. . . . . . 7
28	8, 27	eqssi 3372	. . . . . 6
29	28	imaeq2i 5167	. . . . 5
30	4, 29	eqtr3i 2465	. . . 4
31		ismbf3d.2	. . . . . . . 8 $/\$
32	31	ralrimiva 2799	. . . . . . 7
33	14	renegcld 9775	. . . . . . 7
34		oveq1 6098	. . . . . . . . . 10
35	34	imaeq2d 5169	. . . . . . . . 9
36	35	eleq1d 2509	. . . . . . . 8
37	36	rspccva 3072	. . . . . . 7 $/\$
38	32, 33, 37	syl2an 477	. . . . . 6 $/\$
39	38	ralrimiva 2799	. . . . 5
40		iunmbl 21034	. . . . 5
41	39, 40	syl 16	. . . 4
42	30, 41	syl5eqelr 2528	. . 3
43	3, 42	eqeltrrd 2518	. 2
44		imaiun 5962	. . . . . . 7
45		eliun 4175	. . . . . . . . . 10
46		3simpb 986	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
47		simplr 754	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
48		nnrp 11000	. . . . . . . . . . . . . . . . . . . . . 22
49	48	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
50	49	rpreccld 11037	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
51	47, 50	ltsubrpd 11055	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
52		simprr 756	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
53		simpr 461	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
54		nnrecre 10358	. . . . . . . . . . . . . . . . . . . . . 22
55		resubcl 9673	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
56	53, 54, 55	syl2an 477	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
57	56	adantrr 716	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
58		lelttr 9465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
59	52, 57, 47, 58	syl3anc 1218	. . . . . . . . . . . . . . . . . . 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 11094	. . . . . . . . . . . . . . . 16
65		elioc2 11358	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
66	64, 56, 65	sylancr 663	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
67		rexr 9429	. . . . . . . . . . . . . . . . . 18
68	67	adantl 466	. . . . . . . . . . . . . . . . 17 $/\$
69		elioomnf 11384	. . . . . . . . . . . . . . . . 17 $/\$
70	68, 69	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
71	70	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
72	63, 66, 71	3imtr4d 268	. . . . . . . . . . . . . 14 $/\$ $/\$
73	72	rexlimdva 2841	. . . . . . . . . . . . 13 $/\$
74	73, 70	sylibd 214	. . . . . . . . . . . 12 $/\$ $/\$
75		simplr 754	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
76		simprl 755	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
77	75, 76	resubcld 9776	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
78		simprr 756	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
79	76, 75	posdifd 9926	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
80	78, 79	mpbid 210	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
81		nnrecl 10577	. . . . . . . . . . . . . . 15 $/\$
82	77, 80, 81	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
83	76	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
84		mnflt 11104	. . . . . . . . . . . . . . . . . 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 9945	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
91	83, 86, 90	ltled 9522	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
92	66	ad2ant2r 746	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
93	83, 85, 91, 92	mpbir3and 1171	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
94	93	expr 615	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
95	94	reximdva 2828	. . . . . . . . . . . . . 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 2441	. . . . . . . 8 $/\$
102	101	imaeq2d 5169	. . . . . . 7 $/\$
103	44, 102	syl5eqr 2489	. . . . . 6 $/\$
104	1	ad2antrr 725	. . . . . . . . . . 11 $/\$ $/\$
105		ffun 5561	. . . . . . . . . . 11
106		funcnvcnv 5476	. . . . . . . . . . 11
107		imadif 5493	. . . . . . . . . . 11 $\$ $\$
108	104, 105, 106, 107	4syl 21	. . . . . . . . . 10 $/\$ $/\$ $\$ $\$
109	64	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
110	56	rexrd 9433	. . . . . . . . . . . . . 14 $/\$ $/\$
111		pnfxr 11092	. . . . . . . . . . . . . . 15
112	111	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
113		mnflt 11104	. . . . . . . . . . . . . . 15
114	56, 113	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$
115		ltpnf 11102	. . . . . . . . . . . . . . 15
116	56, 115	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$
117		df-ioc 11305	. . . . . . . . . . . . . . 15 $/\$
118		df-ioo 11304	. . . . . . . . . . . . . . 15 $/\$
119		xrltnle 9443	. . . . . . . . . . . . . . 15 $/\$
120		xrlelttr 11130	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
121		xrlttr 11117	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
122	117, 118, 119, 118, 120, 121	ixxun 11316	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
123	109, 110, 112, 114, 116, 122	syl32anc 1226	. . . . . . . . . . . . 13 $/\$ $/\$
124		uncom 3500	. . . . . . . . . . . . 13
125		ioomax 11370	. . . . . . . . . . . . 13
126	123, 124, 125	3eqtr3g 2498	. . . . . . . . . . . 12 $/\$ $/\$
127		ioossre 11357	. . . . . . . . . . . . 13
128		incom 3543	. . . . . . . . . . . . . 14
129	117, 118, 119	ixxdisj 11315	. . . . . . . . . . . . . . . 16 $/\$ $/\$
130	64, 111, 129	mp3an13 1305	. . . . . . . . . . . . . . 15
131	110, 130	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$
132	128, 131	syl5eq 2487	. . . . . . . . . . . . 13 $/\$ $/\$
133		uneqdifeq 3767	. . . . . . . . . . . . 13 $/\$ $\$
134	127, 132, 133	sylancr 663	. . . . . . . . . . . 12 $/\$ $/\$ $\$
135	126, 134	mpbid 210	. . . . . . . . . . 11 $/\$ $/\$ $\$
136	135	imaeq2d 5169	. . . . . . . . . 10 $/\$ $/\$ $\$
137	108, 136	eqtr3d 2477	. . . . . . . . 9 $/\$ $/\$ $\$
138	42	ad2antrr 725	. . . . . . . . . 10 $/\$ $/\$
139	32	ad2antrr 725	. . . . . . . . . . 11 $/\$ $/\$
140		oveq1 6098	. . . . . . . . . . . . . 14
141	140	imaeq2d 5169	. . . . . . . . . . . . 13
142	141	eleq1d 2509	. . . . . . . . . . . 12
143	142	rspcv 3069	. . . . . . . . . . 11
144	56, 139, 143	sylc 60	. . . . . . . . . 10 $/\$ $/\$
145		difmbl 21024	. . . . . . . . . 10 $/\$ $\$
146	138, 144, 145	syl2anc 661	. . . . . . . . 9 $/\$ $/\$ $\$
147	137, 146	eqeltrrd 2518	. . . . . . . 8 $/\$ $/\$
148	147	ralrimiva 2799	. . . . . . 7 $/\$
149		iunmbl 21034	. . . . . . 7
150	148, 149	syl 16	. . . . . 6 $/\$
151	103, 150	eqeltrrd 2518	. . . . 5 $/\$
152	151	ralrimiva 2799	. . . 4
153		oveq2 6099	. . . . . . 7
154	153	imaeq2d 5169	. . . . . 6
155	154	eleq1d 2509	. . . . 5
156	155	cbvralv 2947	. . . 4
157	152, 156	sylib 196	. . 3
158	157	r19.21bi 2814	. 2 $/\$
159	1, 43, 31, 158	ismbf2d 21119	1 MblFn

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1369

wcel 1756

wral 2715

wrex 2716 $\$ cdif 3325

cun 3326

cin 3327

wss 3328

c0 3637

ciun 4171 class class class wbr 4292

ccnv 4839

cdm 4840

cima 4843

wfun 5412

wf 5414 (class class class)co 6091

cr 9281

cc0 9282

c1 9283

cpnf 9415

cmnf 9416

cxr 9417

clt 9418

cle 9419

cmin 9595

cneg 9596

cdiv 9993

cn 10322

crp 10991

cioo 11300

cioc 11301

cvol 20947 MblFncmbf 21094

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-rep 4403 ax-sep 4413 ax-nul 4421 ax-pow 4470 ax-pr 4531 ax-un 6372 ax-inf2 7847 ax-cc 8604 ax-cnex 9338 ax-resscn 9339 ax-1cn 9340 ax-icn 9341 ax-addcl 9342 ax-addrcl 9343 ax-mulcl 9344 ax-mulrcl 9345 ax-mulcom 9346 ax-addass 9347 ax-mulass 9348 ax-distr 9349 ax-i2m1 9350 ax-1ne0 9351 ax-1rid 9352 ax-rnegex 9353 ax-rrecex 9354 ax-cnre 9355 ax-pre-lttri 9356 ax-pre-lttrn 9357 ax-pre-ltadd 9358 ax-pre-mulgt0 9359 ax-pre-sup 9360

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-fal 1375 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 2568 df-ne 2608 df-nel 2609 df-ral 2720 df-rex 2721 df-reu 2722 df-rmo 2723 df-rab 2724 df-v 2974 df-sbc 3187 df-csb 3289 df-dif 3331 df-un 3333 df-in 3335 df-ss 3342 df-pss 3344 df-nul 3638 df-if 3792 df-pw 3862 df-sn 3878 df-pr 3880 df-tp 3882 df-op 3884 df-uni 4092 df-int 4129 df-iun 4173 df-disj 4263 df-br 4293 df-opab 4351 df-mpt 4352 df-tr 4386 df-eprel 4632 df-id 4636 df-po 4641 df-so 4642 df-fr 4679 df-se 4680 df-we 4681 df-ord 4722 df-on 4723 df-lim 4724 df-suc 4725 df-xp 4846 df-rel 4847 df-cnv 4848 df-co 4849 df-dm 4850 df-rn 4851 df-res 4852 df-ima 4853 df-iota 5381 df-fun 5420 df-fn 5421 df-f 5422 df-f1 5423 df-fo 5424 df-f1o 5425 df-fv 5426 df-isom 5427 df-riota 6052 df-ov 6094 df-oprab 6095 df-mpt2 6096 df-of 6320 df-om 6477 df-1st 6577 df-2nd 6578 df-recs 6832 df-rdg 6866 df-1o 6920 df-2o 6921 df-oadd 6924 df-er 7101 df-map 7216 df-pm 7217 df-en 7311 df-dom 7312 df-sdom 7313 df-fin 7314 df-sup 7691 df-oi 7724 df-card 8109 df-cda 8337 df-pnf 9420 df-mnf 9421 df-xr 9422 df-ltxr 9423 df-le 9424 df-sub 9597 df-neg 9598 df-div 9994 df-nn 10323 df-2 10380 df-3 10381 df-n0 10580 df-z 10647 df-uz 10862 df-q 10954 df-rp 10992 df-xadd 11090 df-ioo 11304 df-ioc 11305 df-ico 11306 df-icc 11307 df-fz 11438 df-fzo 11549 df-fl 11642 df-seq 11807 df-exp 11866 df-hash 12104 df-cj 12588 df-re 12589 df-im 12590 df-sqr 12724 df-abs 12725 df-clim 12966 df-rlim 12967 df-sum 13164 df-xmet 17810 df-met 17811 df-ovol 20948 df-vol 20949 df-mbf 21099

This theorem is referenced by: mbfaddlem 21138 mbfsup 21142

W3C validator