ismbf3d - Metamath Proof Explorer

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

Theorem ismbf3d 19499

Description: Simplified form of ismbfd 19485. (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 5821	. . . 4
3	1, 2	syl 16	. . 3
4		imaiun 5951	. . . . 5
5		ioossre 10928	. . . . . . . . 9
6	5	rgenw 2733	. . . . . . . 8
7		iunss 4092	. . . . . . . 8
8	6, 7	mpbir 201	. . . . . . 7
9		renegcl 9320	. . . . . . . . . . 11
10		arch 10174	. . . . . . . . . . 11
11	9, 10	syl 16	. . . . . . . . . 10
12		simpl 444	. . . . . . . . . . . . 13 $/\$
13	12	biantrurd 495	. . . . . . . . . . . 12 $/\$ $/\$
14		nnre 9963	. . . . . . . . . . . . 13
15		ltnegcon1 9485	. . . . . . . . . . . . 13 $/\$
16	14, 15	sylan2 461	. . . . . . . . . . . 12 $/\$
17	14	adantl 453	. . . . . . . . . . . . . . 15 $/\$
18	17	renegcld 9420	. . . . . . . . . . . . . 14 $/\$
19	18	rexrd 9090	. . . . . . . . . . . . 13 $/\$
20		elioopnf 10954	. . . . . . . . . . . . 13 $/\$
21	19, 20	syl 16	. . . . . . . . . . . 12 $/\$ $/\$
22	13, 16, 21	3bitr4d 277	. . . . . . . . . . 11 $/\$
23	22	rexbidva 2683	. . . . . . . . . 10
24	11, 23	mpbid 202	. . . . . . . . 9
25		eliun 4057	. . . . . . . . 9
26	24, 25	sylibr 204	. . . . . . . 8
27	26	ssriv 3312	. . . . . . 7
28	8, 27	eqssi 3324	. . . . . 6
29	28	imaeq2i 5160	. . . . 5
30	4, 29	eqtr3i 2426	. . . 4
31		ismbf3d.2	. . . . . . . 8 $/\$
32	31	ralrimiva 2749	. . . . . . 7
33	14	renegcld 9420	. . . . . . 7
34		oveq1 6047	. . . . . . . . . 10
35	34	imaeq2d 5162	. . . . . . . . 9
36	35	eleq1d 2470	. . . . . . . 8
37	36	rspccva 3011	. . . . . . 7 $/\$
38	32, 33, 37	syl2an 464	. . . . . 6 $/\$
39	38	ralrimiva 2749	. . . . 5
40		iunmbl 19400	. . . . 5
41	39, 40	syl 16	. . . 4
42	30, 41	syl5eqelr 2489	. . 3
43	3, 42	eqeltrrd 2479	. 2
44		imaiun 5951	. . . . . . 7
45		eliun 4057	. . . . . . . . . 10
46		3simpb 955	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
47		simplr 732	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
48		nnrp 10577	. . . . . . . . . . . . . . . . . . . . . 22
49	48	ad2antrl 709	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
50	49	rpreccld 10614	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
51	47, 50	ltsubrpd 10632	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
52		simprr 734	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
53		simpr 448	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
54		nnrecre 9992	. . . . . . . . . . . . . . . . . . . . . 22
55		resubcl 9321	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
56	53, 54, 55	syl2an 464	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
57	56	adantrr 698	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
58		lelttr 9121	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
59	52, 57, 47, 58	syl3anc 1184	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
60	51, 59	mpan2d 656	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
61	60	anassrs 630	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
62	61	imdistanda 675	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
63	46, 62	syl5 30	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
64		mnfxr 10670	. . . . . . . . . . . . . . . 16
65		elioc2 10929	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
66	64, 56, 65	sylancr 645	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
67		rexr 9086	. . . . . . . . . . . . . . . . . 18
68	67	adantl 453	. . . . . . . . . . . . . . . . 17 $/\$
69		elioomnf 10955	. . . . . . . . . . . . . . . . 17 $/\$
70	68, 69	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
71	70	adantr 452	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
72	63, 66, 71	3imtr4d 260	. . . . . . . . . . . . . 14 $/\$ $/\$
73	72	rexlimdva 2790	. . . . . . . . . . . . 13 $/\$
74	73, 70	sylibd 206	. . . . . . . . . . . 12 $/\$ $/\$
75		simplr 732	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
76		simprl 733	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
77	75, 76	resubcld 9421	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
78		simprr 734	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
79	76, 75	posdifd 9569	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
80	78, 79	mpbid 202	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
81		nnrecl 10175	. . . . . . . . . . . . . . 15 $/\$
82	77, 80, 81	syl2anc 643	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
83	76	adantr 452	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
84		mnflt 10678	. . . . . . . . . . . . . . . . . 18
85	83, 84	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
86	56	ad2ant2r 728	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
87	54	ad2antrl 709	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
88	75	adantr 452	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
89		simprr 734	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
90	87, 88, 83, 89	ltsub13d 9588	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
91	83, 86, 90	ltled 9177	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
92	66	ad2ant2r 728	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
93	83, 85, 91, 92	mpbir3and 1137	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
94	93	expr 599	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
95	94	reximdva 2778	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
96	82, 95	mpd 15	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
97	96	ex 424	. . . . . . . . . . . 12 $/\$ $/\$
98	74, 97	impbid 184	. . . . . . . . . . 11 $/\$ $/\$
99	98, 70	bitr4d 248	. . . . . . . . . 10 $/\$
100	45, 99	syl5bb 249	. . . . . . . . 9 $/\$
101	100	eqrdv 2402	. . . . . . . 8 $/\$
102	101	imaeq2d 5162	. . . . . . 7 $/\$
103	44, 102	syl5eqr 2450	. . . . . 6 $/\$
104	1	ad2antrr 707	. . . . . . . . . . . 12 $/\$ $/\$
105		ffun 5552	. . . . . . . . . . . 12
106	104, 105	syl 16	. . . . . . . . . . 11 $/\$ $/\$
107		funcnvcnv 5468	. . . . . . . . . . 11
108		imadif 5487	. . . . . . . . . . 11 $\$ $\$
109	106, 107, 108	3syl 19	. . . . . . . . . 10 $/\$ $/\$ $\$ $\$
110	64	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
111	56	rexrd 9090	. . . . . . . . . . . . . 14 $/\$ $/\$
112		pnfxr 10669	. . . . . . . . . . . . . . 15
113	112	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
114		mnflt 10678	. . . . . . . . . . . . . . 15
115	56, 114	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$
116		ltpnf 10677	. . . . . . . . . . . . . . 15
117	56, 116	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$
118		df-ioc 10877	. . . . . . . . . . . . . . 15 $/\$
119		df-ioo 10876	. . . . . . . . . . . . . . 15 $/\$
120		xrltnle 9100	. . . . . . . . . . . . . . 15 $/\$
121		xrlelttr 10702	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
122		xrlttr 10689	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
123	118, 119, 120, 119, 121, 122	ixxun 10888	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
124	110, 111, 113, 115, 117, 123	syl32anc 1192	. . . . . . . . . . . . 13 $/\$ $/\$
125		uncom 3451	. . . . . . . . . . . . 13
126		ioomax 10941	. . . . . . . . . . . . 13
127	124, 125, 126	3eqtr3g 2459	. . . . . . . . . . . 12 $/\$ $/\$
128		ioossre 10928	. . . . . . . . . . . . 13
129		incom 3493	. . . . . . . . . . . . . 14
130	118, 119, 120	ixxdisj 10887	. . . . . . . . . . . . . . . 16 $/\$ $/\$
131	64, 112, 130	mp3an13 1270	. . . . . . . . . . . . . . 15
132	111, 131	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$
133	129, 132	syl5eq 2448	. . . . . . . . . . . . 13 $/\$ $/\$
134		uneqdifeq 3676	. . . . . . . . . . . . 13 $/\$ $\$
135	128, 133, 134	sylancr 645	. . . . . . . . . . . 12 $/\$ $/\$ $\$
136	127, 135	mpbid 202	. . . . . . . . . . 11 $/\$ $/\$ $\$
137	136	imaeq2d 5162	. . . . . . . . . 10 $/\$ $/\$ $\$
138	109, 137	eqtr3d 2438	. . . . . . . . 9 $/\$ $/\$ $\$
139	42	ad2antrr 707	. . . . . . . . . 10 $/\$ $/\$
140	32	ad2antrr 707	. . . . . . . . . . 11 $/\$ $/\$
141		oveq1 6047	. . . . . . . . . . . . . 14
142	141	imaeq2d 5162	. . . . . . . . . . . . 13
143	142	eleq1d 2470	. . . . . . . . . . . 12
144	143	rspcv 3008	. . . . . . . . . . 11
145	56, 140, 144	sylc 58	. . . . . . . . . 10 $/\$ $/\$
146		difmbl 19390	. . . . . . . . . 10 $/\$ $\$
147	139, 145, 146	syl2anc 643	. . . . . . . . 9 $/\$ $/\$ $\$
148	138, 147	eqeltrrd 2479	. . . . . . . 8 $/\$ $/\$
149	148	ralrimiva 2749	. . . . . . 7 $/\$
150		iunmbl 19400	. . . . . . 7
151	149, 150	syl 16	. . . . . 6 $/\$
152	103, 151	eqeltrrd 2479	. . . . 5 $/\$
153	152	ralrimiva 2749	. . . 4
154		oveq2 6048	. . . . . . 7
155	154	imaeq2d 5162	. . . . . 6
156	155	eleq1d 2470	. . . . 5
157	156	cbvralv 2892	. . . 4
158	153, 157	sylib 189	. . 3
159	158	r19.21bi 2764	. 2 $/\$
160	1, 43, 31, 159	ismbf2d 19486	1 MblFn

Colors of variables: wff set class

Syntax hints:

wi 4

wb 177 $/\$ wa 359 $/\$ w3a 936

wceq 1649

wcel 1721

wral 2666

wrex 2667 $\$ cdif 3277

cun 3278

cin 3279

wss 3280

c0 3588

ciun 4053 class class class wbr 4172

ccnv 4836

cdm 4837

cima 4840

wfun 5407

wf 5409 (class class class)co 6040

cr 8945

cc0 8946

c1 8947

cpnf 9073

cmnf 9074

cxr 9075

clt 9076

cle 9077

cmin 9247

cneg 9248

cdiv 9633

cn 9956

crp 10568

cioo 10872

cioc 10873

cvol 19313 MblFncmbf 19459

This theorem is referenced by: mbfaddlem 19505 mbfsup 19509

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-rep 4280 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-inf2 7552 ax-cc 8271 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023 ax-pre-sup 9024

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-int 4011 df-iun 4055 df-disj 4143 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-se 4502 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-isom 5422 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-of 6264 df-1st 6308 df-2nd 6309 df-riota 6508 df-recs 6592 df-rdg 6627 df-1o 6683 df-2o 6684 df-oadd 6687 df-er 6864 df-map 6979 df-pm 6980 df-en 7069 df-dom 7070 df-sdom 7071 df-fin 7072 df-sup 7404 df-oi 7435 df-card 7782 df-cda 8004 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-div 9634 df-nn 9957 df-2 10014 df-3 10015 df-n0 10178 df-z 10239 df-uz 10445 df-q 10531 df-rp 10569 df-xadd 10667 df-ioo 10876 df-ioc 10877 df-ico 10878 df-icc 10879 df-fz 11000 df-fzo 11091 df-fl 11157 df-seq 11279 df-exp 11338 df-hash 11574 df-cj 11859 df-re 11860 df-im 11861 df-sqr 11995 df-abs 11996 df-clim 12237 df-rlim 12238 df-sum 12435 df-xmet 16650 df-met 16651 df-ovol 19314 df-vol 19315 df-mbf 19465

W3C validator