ismbf3d - Metamath Proof Explorer

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

Theorem ismbf3d 21032

Description: Simplified form of ismbfd 21018. (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 5832	. . . 4
3	1, 2	syl 16	. . 3
4		imaiun 5959	. . . . 5
5		ioossre 11353	. . . . . . . . 9
6	5	rgenw 2781	. . . . . . . 8
7		iunss 4208	. . . . . . . 8
8	6, 7	mpbir 209	. . . . . . 7
9		renegcl 9668	. . . . . . . . . . 11
10		arch 10572	. . . . . . . . . . 11
11	9, 10	syl 16	. . . . . . . . . 10
12		simpl 454	. . . . . . . . . . . . 13 $/\$
13	12	biantrurd 505	. . . . . . . . . . . 12 $/\$ $/\$
14		nnre 10325	. . . . . . . . . . . . 13
15		ltnegcon1 9836	. . . . . . . . . . . . 13 $/\$
16	14, 15	sylan2 471	. . . . . . . . . . . 12 $/\$
17	14	adantl 463	. . . . . . . . . . . . . . 15 $/\$
18	17	renegcld 9771	. . . . . . . . . . . . . 14 $/\$
19	18	rexrd 9429	. . . . . . . . . . . . 13 $/\$
20		elioopnf 11379	. . . . . . . . . . . . 13 $/\$
21	19, 20	syl 16	. . . . . . . . . . . 12 $/\$ $/\$
22	13, 16, 21	3bitr4d 285	. . . . . . . . . . 11 $/\$
23	22	rexbidva 2730	. . . . . . . . . 10
24	11, 23	mpbid 210	. . . . . . . . 9
25		eliun 4172	. . . . . . . . 9
26	24, 25	sylibr 212	. . . . . . . 8
27	26	ssriv 3357	. . . . . . 7
28	8, 27	eqssi 3369	. . . . . 6
29	28	imaeq2i 5164	. . . . 5
30	4, 29	eqtr3i 2463	. . . 4
31		ismbf3d.2	. . . . . . . 8 $/\$
32	31	ralrimiva 2797	. . . . . . 7
33	14	renegcld 9771	. . . . . . 7
34		oveq1 6097	. . . . . . . . . 10
35	34	imaeq2d 5166	. . . . . . . . 9
36	35	eleq1d 2507	. . . . . . . 8
37	36	rspccva 3069	. . . . . . 7 $/\$
38	32, 33, 37	syl2an 474	. . . . . 6 $/\$
39	38	ralrimiva 2797	. . . . 5
40		iunmbl 20934	. . . . 5
41	39, 40	syl 16	. . . 4
42	30, 41	syl5eqelr 2526	. . 3
43	3, 42	eqeltrrd 2516	. 2
44		imaiun 5959	. . . . . . 7
45		eliun 4172	. . . . . . . . . 10
46		3simpb 981	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
47		simplr 749	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
48		nnrp 10996	. . . . . . . . . . . . . . . . . . . . . 22
49	48	ad2antrl 722	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
50	49	rpreccld 11033	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
51	47, 50	ltsubrpd 11051	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
52		simprr 751	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
53		simpr 458	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
54		nnrecre 10354	. . . . . . . . . . . . . . . . . . . . . 22
55		resubcl 9669	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
56	53, 54, 55	syl2an 474	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
57	56	adantrr 711	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
58		lelttr 9461	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
59	52, 57, 47, 58	syl3anc 1213	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
60	51, 59	mpan2d 669	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
61	60	anassrs 643	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
62	61	imdistanda 688	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
63	46, 62	syl5 32	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
64		mnfxr 11090	. . . . . . . . . . . . . . . 16
65		elioc2 11354	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
66	64, 56, 65	sylancr 658	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
67		rexr 9425	. . . . . . . . . . . . . . . . . 18
68	67	adantl 463	. . . . . . . . . . . . . . . . 17 $/\$
69		elioomnf 11380	. . . . . . . . . . . . . . . . 17 $/\$
70	68, 69	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
71	70	adantr 462	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
72	63, 66, 71	3imtr4d 268	. . . . . . . . . . . . . 14 $/\$ $/\$
73	72	rexlimdva 2839	. . . . . . . . . . . . 13 $/\$
74	73, 70	sylibd 214	. . . . . . . . . . . 12 $/\$ $/\$
75		simplr 749	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
76		simprl 750	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
77	75, 76	resubcld 9772	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
78		simprr 751	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
79	76, 75	posdifd 9922	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
80	78, 79	mpbid 210	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
81		nnrecl 10573	. . . . . . . . . . . . . . 15 $/\$
82	77, 80, 81	syl2anc 656	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
83	76	adantr 462	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
84		mnflt 11100	. . . . . . . . . . . . . . . . . 18
85	83, 84	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
86	56	ad2ant2r 741	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
87	54	ad2antrl 722	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
88	75	adantr 462	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
89		simprr 751	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
90	87, 88, 83, 89	ltsub13d 9941	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
91	83, 86, 90	ltled 9518	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
92	66	ad2ant2r 741	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
93	83, 85, 91, 92	mpbir3and 1166	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
94	93	expr 612	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
95	94	reximdva 2826	. . . . . . . . . . . . . 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 2439	. . . . . . . 8 $/\$
102	101	imaeq2d 5166	. . . . . . 7 $/\$
103	44, 102	syl5eqr 2487	. . . . . 6 $/\$
104	1	ad2antrr 720	. . . . . . . . . . 11 $/\$ $/\$
105		ffun 5558	. . . . . . . . . . 11
106		funcnvcnv 5473	. . . . . . . . . . 11
107		imadif 5490	. . . . . . . . . . 11 $\$ $\$
108	104, 105, 106, 107	4syl 21	. . . . . . . . . 10 $/\$ $/\$ $\$ $\$
109	64	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
110	56	rexrd 9429	. . . . . . . . . . . . . 14 $/\$ $/\$
111		pnfxr 11088	. . . . . . . . . . . . . . 15
112	111	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
113		mnflt 11100	. . . . . . . . . . . . . . 15
114	56, 113	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$
115		ltpnf 11098	. . . . . . . . . . . . . . 15
116	56, 115	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$
117		df-ioc 11301	. . . . . . . . . . . . . . 15 $/\$
118		df-ioo 11300	. . . . . . . . . . . . . . 15 $/\$
119		xrltnle 9439	. . . . . . . . . . . . . . 15 $/\$
120		xrlelttr 11126	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
121		xrlttr 11113	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
122	117, 118, 119, 118, 120, 121	ixxun 11312	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
123	109, 110, 112, 114, 116, 122	syl32anc 1221	. . . . . . . . . . . . 13 $/\$ $/\$
124		uncom 3497	. . . . . . . . . . . . 13
125		ioomax 11366	. . . . . . . . . . . . 13
126	123, 124, 125	3eqtr3g 2496	. . . . . . . . . . . 12 $/\$ $/\$
127		ioossre 11353	. . . . . . . . . . . . 13
128		incom 3540	. . . . . . . . . . . . . 14
129	117, 118, 119	ixxdisj 11311	. . . . . . . . . . . . . . . 16 $/\$ $/\$
130	64, 111, 129	mp3an13 1300	. . . . . . . . . . . . . . 15
131	110, 130	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$
132	128, 131	syl5eq 2485	. . . . . . . . . . . . 13 $/\$ $/\$
133		uneqdifeq 3764	. . . . . . . . . . . . 13 $/\$ $\$
134	127, 132, 133	sylancr 658	. . . . . . . . . . . 12 $/\$ $/\$ $\$
135	126, 134	mpbid 210	. . . . . . . . . . 11 $/\$ $/\$ $\$
136	135	imaeq2d 5166	. . . . . . . . . 10 $/\$ $/\$ $\$
137	108, 136	eqtr3d 2475	. . . . . . . . 9 $/\$ $/\$ $\$
138	42	ad2antrr 720	. . . . . . . . . 10 $/\$ $/\$
139	32	ad2antrr 720	. . . . . . . . . . 11 $/\$ $/\$
140		oveq1 6097	. . . . . . . . . . . . . 14
141	140	imaeq2d 5166	. . . . . . . . . . . . 13
142	141	eleq1d 2507	. . . . . . . . . . . 12
143	142	rspcv 3066	. . . . . . . . . . 11
144	56, 139, 143	sylc 60	. . . . . . . . . 10 $/\$ $/\$
145		difmbl 20924	. . . . . . . . . 10 $/\$ $\$
146	138, 144, 145	syl2anc 656	. . . . . . . . 9 $/\$ $/\$ $\$
147	137, 146	eqeltrrd 2516	. . . . . . . 8 $/\$ $/\$
148	147	ralrimiva 2797	. . . . . . 7 $/\$
149		iunmbl 20934	. . . . . . 7
150	148, 149	syl 16	. . . . . 6 $/\$
151	103, 150	eqeltrrd 2516	. . . . 5 $/\$
152	151	ralrimiva 2797	. . . 4
153		oveq2 6098	. . . . . . 7
154	153	imaeq2d 5166	. . . . . 6
155	154	eleq1d 2507	. . . . 5
156	155	cbvralv 2945	. . . 4
157	152, 156	sylib 196	. . 3
158	157	r19.21bi 2812	. 2 $/\$
159	1, 43, 31, 158	ismbf2d 21019	1 MblFn

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1364

wcel 1761

wral 2713

wrex 2714 $\$ cdif 3322

cun 3323

cin 3324

wss 3325

c0 3634

ciun 4168 class class class wbr 4289

ccnv 4835

cdm 4836

cima 4839

wfun 5409

wf 5411 (class class class)co 6090

cr 9277

cc0 9278

c1 9279

cpnf 9411

cmnf 9412

cxr 9413

clt 9414

cle 9415

cmin 9591

cneg 9592

cdiv 9989

cn 10318

crp 10987

cioo 11296

cioc 11297

cvol 20847 MblFncmbf 20994

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1713 ax-7 1733 ax-8 1763 ax-9 1765 ax-10 1780 ax-11 1785 ax-12 1797 ax-13 1948 ax-ext 2422 ax-rep 4400 ax-sep 4410 ax-nul 4418 ax-pow 4467 ax-pr 4528 ax-un 6371 ax-inf2 7843 ax-cc 8600 ax-cnex 9334 ax-resscn 9335 ax-1cn 9336 ax-icn 9337 ax-addcl 9338 ax-addrcl 9339 ax-mulcl 9340 ax-mulrcl 9341 ax-mulcom 9342 ax-addass 9343 ax-mulass 9344 ax-distr 9345 ax-i2m1 9346 ax-1ne0 9347 ax-1rid 9348 ax-rnegex 9349 ax-rrecex 9350 ax-cnre 9351 ax-pre-lttri 9352 ax-pre-lttrn 9353 ax-pre-ltadd 9354 ax-pre-mulgt0 9355 ax-pre-sup 9356

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 961 df-3an 962 df-tru 1367 df-fal 1370 df-ex 1592 df-nf 1595 df-sb 1706 df-eu 2263 df-mo 2264 df-clab 2428 df-cleq 2434 df-clel 2437 df-nfc 2566 df-ne 2606 df-nel 2607 df-ral 2718 df-rex 2719 df-reu 2720 df-rmo 2721 df-rab 2722 df-v 2972 df-sbc 3184 df-csb 3286 df-dif 3328 df-un 3330 df-in 3332 df-ss 3339 df-pss 3341 df-nul 3635 df-if 3789 df-pw 3859 df-sn 3875 df-pr 3877 df-tp 3879 df-op 3881 df-uni 4089 df-int 4126 df-iun 4170 df-disj 4260 df-br 4290 df-opab 4348 df-mpt 4349 df-tr 4383 df-eprel 4628 df-id 4632 df-po 4637 df-so 4638 df-fr 4675 df-se 4676 df-we 4677 df-ord 4718 df-on 4719 df-lim 4720 df-suc 4721 df-xp 4842 df-rel 4843 df-cnv 4844 df-co 4845 df-dm 4846 df-rn 4847 df-res 4848 df-ima 4849 df-iota 5378 df-fun 5417 df-fn 5418 df-f 5419 df-f1 5420 df-fo 5421 df-f1o 5422 df-fv 5423 df-isom 5424 df-riota 6049 df-ov 6093 df-oprab 6094 df-mpt2 6095 df-of 6319 df-om 6476 df-1st 6576 df-2nd 6577 df-recs 6828 df-rdg 6862 df-1o 6916 df-2o 6917 df-oadd 6920 df-er 7097 df-map 7212 df-pm 7213 df-en 7307 df-dom 7308 df-sdom 7309 df-fin 7310 df-sup 7687 df-oi 7720 df-card 8105 df-cda 8333 df-pnf 9416 df-mnf 9417 df-xr 9418 df-ltxr 9419 df-le 9420 df-sub 9593 df-neg 9594 df-div 9990 df-nn 10319 df-2 10376 df-3 10377 df-n0 10576 df-z 10643 df-uz 10858 df-q 10950 df-rp 10988 df-xadd 11086 df-ioo 11300 df-ioc 11301 df-ico 11302 df-icc 11303 df-fz 11434 df-fzo 11545 df-fl 11638 df-seq 11803 df-exp 11862 df-hash 12100 df-cj 12584 df-re 12585 df-im 12586 df-sqr 12720 df-abs 12721 df-clim 12962 df-rlim 12963 df-sum 13160 df-xmet 17710 df-met 17711 df-ovol 20848 df-vol 20849 df-mbf 20999

This theorem is referenced by: mbfaddlem 21038 mbfsup 21042

W3C validator