ismbf3d - Metamath Proof Explorer

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

Theorem ismbf3d 22187

Description: Simplified form of ismbfd 22173. (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 6020	. . . 4
3	1, 2	syl 16	. . 3
4		imaiun 6158	. . . . 5
5		ioossre 11611	. . . . . . . . 9
6	5	rgenw 2818	. . . . . . . 8
7		iunss 4373	. . . . . . . 8
8	6, 7	mpbir 209	. . . . . . 7
9		renegcl 9901	. . . . . . . . . . 11
10		arch 10813	. . . . . . . . . . 11
11	9, 10	syl 16	. . . . . . . . . 10
12		simpl 457	. . . . . . . . . . . . 13 $/\$
13	12	biantrurd 508	. . . . . . . . . . . 12 $/\$ $/\$
14		nnre 10563	. . . . . . . . . . . . 13
15		ltnegcon1 10074	. . . . . . . . . . . . 13 $/\$
16	14, 15	sylan2 474	. . . . . . . . . . . 12 $/\$
17	14	adantl 466	. . . . . . . . . . . . . . 15 $/\$
18	17	renegcld 10007	. . . . . . . . . . . . . 14 $/\$
19	18	rexrd 9660	. . . . . . . . . . . . 13 $/\$
20		elioopnf 11643	. . . . . . . . . . . . 13 $/\$
21	19, 20	syl 16	. . . . . . . . . . . 12 $/\$ $/\$
22	13, 16, 21	3bitr4d 285	. . . . . . . . . . 11 $/\$
23	22	rexbidva 2965	. . . . . . . . . 10
24	11, 23	mpbid 210	. . . . . . . . 9
25		eliun 4337	. . . . . . . . 9
26	24, 25	sylibr 212	. . . . . . . 8
27	26	ssriv 3503	. . . . . . 7
28	8, 27	eqssi 3515	. . . . . 6
29	28	imaeq2i 5345	. . . . 5
30	4, 29	eqtr3i 2488	. . . 4
31		ismbf3d.2	. . . . . . . 8 $/\$
32	31	ralrimiva 2871	. . . . . . 7
33	14	renegcld 10007	. . . . . . 7
34		oveq1 6303	. . . . . . . . . 10
35	34	imaeq2d 5347	. . . . . . . . 9
36	35	eleq1d 2526	. . . . . . . 8
37	36	rspccva 3209	. . . . . . 7 $/\$
38	32, 33, 37	syl2an 477	. . . . . 6 $/\$
39	38	ralrimiva 2871	. . . . 5
40		iunmbl 22089	. . . . 5
41	39, 40	syl 16	. . . 4
42	30, 41	syl5eqelr 2550	. . 3
43	3, 42	eqeltrrd 2546	. 2
44		imaiun 6158	. . . . . . 7
45		eliun 4337	. . . . . . . . . 10
46		3simpb 994	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
47		simplr 755	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
48		nnrp 11254	. . . . . . . . . . . . . . . . . . . . . 22
49	48	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
50	49	rpreccld 11291	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
51	47, 50	ltsubrpd 11309	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
52		simprr 757	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
53		simpr 461	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
54		nnrecre 10593	. . . . . . . . . . . . . . . . . . . . . 22
55		resubcl 9902	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
56	53, 54, 55	syl2an 477	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
57	56	adantrr 716	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
58		lelttr 9692	. . . . . . . . . . . . . . . . . . . 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 11348	. . . . . . . . . . . . . . . 16
65		elioc2 11612	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
66	64, 56, 65	sylancr 663	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
67		rexr 9656	. . . . . . . . . . . . . . . . . 18
68	67	adantl 466	. . . . . . . . . . . . . . . . 17 $/\$
69		elioomnf 11644	. . . . . . . . . . . . . . . . 17 $/\$
70	68, 69	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
71	70	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
72	63, 66, 71	3imtr4d 268	. . . . . . . . . . . . . 14 $/\$ $/\$
73	72	rexlimdva 2949	. . . . . . . . . . . . 13 $/\$
74	73, 70	sylibd 214	. . . . . . . . . . . 12 $/\$ $/\$
75		simprl 756	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
76	75	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
77		mnflt 11358	. . . . . . . . . . . . . . . 16
78	76, 77	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
79	56	ad2ant2r 746	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
80	54	ad2antrl 727	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
81		simplr 755	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
82	81	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
83		simprr 757	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
84	80, 82, 76, 83	ltsub13d 10179	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
85	76, 79, 84	ltled 9750	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
86	66	ad2ant2r 746	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
87	76, 78, 85, 86	mpbir3and 1179	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
88	81, 75	resubcld 10008	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
89		simprr 757	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
90	75, 81	posdifd 10160	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
91	89, 90	mpbid 210	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
92		nnrecl 10814	. . . . . . . . . . . . . . 15 $/\$
93	88, 91, 92	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
94	87, 93	reximddv 2933	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
95	94	ex 434	. . . . . . . . . . . 12 $/\$ $/\$
96	74, 95	impbid 191	. . . . . . . . . . 11 $/\$ $/\$
97	96, 70	bitr4d 256	. . . . . . . . . 10 $/\$
98	45, 97	syl5bb 257	. . . . . . . . 9 $/\$
99	98	eqrdv 2454	. . . . . . . 8 $/\$
100	99	imaeq2d 5347	. . . . . . 7 $/\$
101	44, 100	syl5eqr 2512	. . . . . 6 $/\$
102	1	ad2antrr 725	. . . . . . . . . . 11 $/\$ $/\$
103		ffun 5739	. . . . . . . . . . 11
104		funcnvcnv 5652	. . . . . . . . . . 11
105		imadif 5669	. . . . . . . . . . 11 $\$ $\$
106	102, 103, 104, 105	4syl 21	. . . . . . . . . 10 $/\$ $/\$ $\$ $\$
107	64	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
108	56	rexrd 9660	. . . . . . . . . . . . . 14 $/\$ $/\$
109		pnfxr 11346	. . . . . . . . . . . . . . 15
110	109	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
111		mnflt 11358	. . . . . . . . . . . . . . 15
112	56, 111	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$
113		ltpnf 11356	. . . . . . . . . . . . . . 15
114	56, 113	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$
115		df-ioc 11559	. . . . . . . . . . . . . . 15 $/\$
116		df-ioo 11558	. . . . . . . . . . . . . . 15 $/\$
117		xrltnle 9670	. . . . . . . . . . . . . . 15 $/\$
118		xrlelttr 11384	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
119		xrlttr 11371	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
120	115, 116, 117, 116, 118, 119	ixxun 11570	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
121	107, 108, 110, 112, 114, 120	syl32anc 1236	. . . . . . . . . . . . 13 $/\$ $/\$
122		uncom 3644	. . . . . . . . . . . . 13
123		ioomax 11624	. . . . . . . . . . . . 13
124	121, 122, 123	3eqtr3g 2521	. . . . . . . . . . . 12 $/\$ $/\$
125		ioossre 11611	. . . . . . . . . . . . 13
126		incom 3687	. . . . . . . . . . . . . 14
127	115, 116, 117	ixxdisj 11569	. . . . . . . . . . . . . . . 16 $/\$ $/\$
128	64, 109, 127	mp3an13 1315	. . . . . . . . . . . . . . 15
129	108, 128	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$
130	126, 129	syl5eq 2510	. . . . . . . . . . . . 13 $/\$ $/\$
131		uneqdifeq 3919	. . . . . . . . . . . . 13 $/\$ $\$
132	125, 130, 131	sylancr 663	. . . . . . . . . . . 12 $/\$ $/\$ $\$
133	124, 132	mpbid 210	. . . . . . . . . . 11 $/\$ $/\$ $\$
134	133	imaeq2d 5347	. . . . . . . . . 10 $/\$ $/\$ $\$
135	106, 134	eqtr3d 2500	. . . . . . . . 9 $/\$ $/\$ $\$
136	42	ad2antrr 725	. . . . . . . . . 10 $/\$ $/\$
137	32	ad2antrr 725	. . . . . . . . . . 11 $/\$ $/\$
138		oveq1 6303	. . . . . . . . . . . . . 14
139	138	imaeq2d 5347	. . . . . . . . . . . . 13
140	139	eleq1d 2526	. . . . . . . . . . . 12
141	140	rspcv 3206	. . . . . . . . . . 11
142	56, 137, 141	sylc 60	. . . . . . . . . 10 $/\$ $/\$
143		difmbl 22079	. . . . . . . . . 10 $/\$ $\$
144	136, 142, 143	syl2anc 661	. . . . . . . . 9 $/\$ $/\$ $\$
145	135, 144	eqeltrrd 2546	. . . . . . . 8 $/\$ $/\$
146	145	ralrimiva 2871	. . . . . . 7 $/\$
147		iunmbl 22089	. . . . . . 7
148	146, 147	syl 16	. . . . . 6 $/\$
149	101, 148	eqeltrrd 2546	. . . . 5 $/\$
150	149	ralrimiva 2871	. . . 4
151		oveq2 6304	. . . . . . 7
152	151	imaeq2d 5347	. . . . . 6
153	152	eleq1d 2526	. . . . 5
154	153	cbvralv 3084	. . . 4
155	150, 154	sylib 196	. . 3
156	155	r19.21bi 2826	. 2 $/\$
157	1, 43, 31, 156	ismbf2d 22174	1 MblFn

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1395

wcel 1819

wral 2807

wrex 2808 $\$ cdif 3468

cun 3469

cin 3470

wss 3471

c0 3793

ciun 4332 class class class wbr 4456

ccnv 5007

cdm 5008

cima 5011

wfun 5588

wf 5590 (class class class)co 6296

cr 9508

cc0 9509

c1 9510

cpnf 9642

cmnf 9643

cxr 9644

clt 9645

cle 9646

cmin 9824

cneg 9825

cdiv 10227

cn 10556

crp 11245

cioo 11554

cioc 11555

cvol 22001 MblFncmbf 22149

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-rep 4568 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-inf2 8075 ax-cc 8832 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586 ax-pre-sup 9587

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-fal 1401 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-int 4289 df-iun 4334 df-disj 4428 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-se 4848 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-isom 5603 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-of 6539 df-om 6700 df-1st 6799 df-2nd 6800 df-recs 7060 df-rdg 7094 df-1o 7148 df-2o 7149 df-oadd 7152 df-er 7329 df-map 7440 df-pm 7441 df-en 7536 df-dom 7537 df-sdom 7538 df-fin 7539 df-sup 7919 df-oi 7953 df-card 8337 df-cda 8565 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-div 10228 df-nn 10557 df-2 10615 df-3 10616 df-n0 10817 df-z 10886 df-uz 11107 df-q 11208 df-rp 11246 df-xadd 11344 df-ioo 11558 df-ioc 11559 df-ico 11560 df-icc 11561 df-fz 11698 df-fzo 11822 df-fl 11932 df-seq 12111 df-exp 12170 df-hash 12409 df-cj 12944 df-re 12945 df-im 12946 df-sqrt 13080 df-abs 13081 df-clim 13323 df-rlim 13324 df-sum 13521 df-xmet 18539 df-met 18540 df-ovol 22002 df-vol 22003 df-mbf 22154

This theorem is referenced by: mbfaddlem 22193 mbfsup 22197

W3C validator