ismbf3d - Metamath Proof Explorer

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

Theorem ismbf3d 22602

Description: Simplified form of ismbfd 22588. (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 6025	. . . 4
3	1, 2	syl 17	. . 3
4		imaiun 6163	. . . . 5
5		ioossre 11698	. . . . . . . . 9
6	5	rgenw 2787	. . . . . . . 8
7		iunss 4338	. . . . . . . 8
8	6, 7	mpbir 213	. . . . . . 7
9		renegcl 9939	. . . . . . . . . . 11
10		arch 10868	. . . . . . . . . . 11
11	9, 10	syl 17	. . . . . . . . . 10
12		simpl 459	. . . . . . . . . . . . 13 $/\$
13	12	biantrurd 511	. . . . . . . . . . . 12 $/\$ $/\$
14		nnre 10618	. . . . . . . . . . . . 13
15		ltnegcon1 10117	. . . . . . . . . . . . 13 $/\$
16	14, 15	sylan2 477	. . . . . . . . . . . 12 $/\$
17	14	adantl 468	. . . . . . . . . . . . . . 15 $/\$
18	17	renegcld 10048	. . . . . . . . . . . . . 14 $/\$
19	18	rexrd 9692	. . . . . . . . . . . . 13 $/\$
20		elioopnf 11730	. . . . . . . . . . . . 13 $/\$
21	19, 20	syl 17	. . . . . . . . . . . 12 $/\$ $/\$
22	13, 16, 21	3bitr4d 289	. . . . . . . . . . 11 $/\$
23	22	rexbidva 2937	. . . . . . . . . 10
24	11, 23	mpbid 214	. . . . . . . . 9
25		eliun 4302	. . . . . . . . 9
26	24, 25	sylibr 216	. . . . . . . 8
27	26	ssriv 3469	. . . . . . 7
28	8, 27	eqssi 3481	. . . . . 6
29	28	imaeq2i 5183	. . . . 5
30	4, 29	eqtr3i 2454	. . . 4
31		ismbf3d.2	. . . . . . . 8 $/\$
32	31	ralrimiva 2840	. . . . . . 7
33	14	renegcld 10048	. . . . . . 7
34		oveq1 6310	. . . . . . . . . 10
35	34	imaeq2d 5185	. . . . . . . . 9
36	35	eleq1d 2492	. . . . . . . 8
37	36	rspccva 3182	. . . . . . 7 $/\$
38	32, 33, 37	syl2an 480	. . . . . 6 $/\$
39	38	ralrimiva 2840	. . . . 5
40		iunmbl 22498	. . . . 5
41	39, 40	syl 17	. . . 4
42	30, 41	syl5eqelr 2516	. . 3
43	3, 42	eqeltrrd 2512	. 2
44		imaiun 6163	. . . . . . 7
45		eliun 4302	. . . . . . . . . 10
46		3simpb 1004	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
47		simplr 761	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
48		nnrp 11313	. . . . . . . . . . . . . . . . . . . . . 22
49	48	ad2antrl 733	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
50	49	rpreccld 11353	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
51	47, 50	ltsubrpd 11372	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
52		simprr 765	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
53		simpr 463	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
54		nnrecre 10648	. . . . . . . . . . . . . . . . . . . . . 22
55		resubcl 9940	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
56	53, 54, 55	syl2an 480	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
57	56	adantrr 722	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
58		lelttr 9726	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
59	52, 57, 47, 58	syl3anc 1265	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
60	51, 59	mpan2d 679	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
61	60	anassrs 653	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
62	61	imdistanda 698	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
63	46, 62	syl5 34	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
64		mnfxr 11416	. . . . . . . . . . . . . . . 16
65		elioc2 11699	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
66	64, 56, 65	sylancr 668	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
67		rexr 9688	. . . . . . . . . . . . . . . . . 18
68	67	adantl 468	. . . . . . . . . . . . . . . . 17 $/\$
69		elioomnf 11731	. . . . . . . . . . . . . . . . 17 $/\$
70	68, 69	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$
71	70	adantr 467	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
72	63, 66, 71	3imtr4d 272	. . . . . . . . . . . . . 14 $/\$ $/\$
73	72	rexlimdva 2918	. . . . . . . . . . . . 13 $/\$
74	73, 70	sylibd 218	. . . . . . . . . . . 12 $/\$ $/\$
75		simprl 763	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
76	75	adantr 467	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
77		mnflt 11427	. . . . . . . . . . . . . . . 16
78	76, 77	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
79	56	ad2ant2r 752	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
80	54	ad2antrl 733	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
81		simplr 761	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
82	81	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
83		simprr 765	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
84	80, 82, 76, 83	ltsub13d 10221	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
85	76, 79, 84	ltled 9785	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
86	66	ad2ant2r 752	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
87	76, 78, 85, 86	mpbir3and 1189	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
88	81, 75	resubcld 10049	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
89		simprr 765	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
90	75, 81	posdifd 10202	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
91	89, 90	mpbid 214	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
92		nnrecl 10869	. . . . . . . . . . . . . . 15 $/\$
93	88, 91, 92	syl2anc 666	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
94	87, 93	reximddv 2902	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
95	94	ex 436	. . . . . . . . . . . 12 $/\$ $/\$
96	74, 95	impbid 194	. . . . . . . . . . 11 $/\$ $/\$
97	96, 70	bitr4d 260	. . . . . . . . . 10 $/\$
98	45, 97	syl5bb 261	. . . . . . . . 9 $/\$
99	98	eqrdv 2420	. . . . . . . 8 $/\$
100	99	imaeq2d 5185	. . . . . . 7 $/\$
101	44, 100	syl5eqr 2478	. . . . . 6 $/\$
102	1	ad2antrr 731	. . . . . . . . . . 11 $/\$ $/\$
103		ffun 5746	. . . . . . . . . . 11
104		funcnvcnv 5657	. . . . . . . . . . 11
105		imadif 5674	. . . . . . . . . . 11 $\$ $\$
106	102, 103, 104, 105	4syl 19	. . . . . . . . . 10 $/\$ $/\$ $\$ $\$
107	64	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
108	56	rexrd 9692	. . . . . . . . . . . . . 14 $/\$ $/\$
109		pnfxr 11414	. . . . . . . . . . . . . . 15
110	109	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
111		mnflt 11427	. . . . . . . . . . . . . . 15
112	56, 111	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$
113		ltpnf 11424	. . . . . . . . . . . . . . 15
114	56, 113	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$
115		df-ioc 11642	. . . . . . . . . . . . . . 15 $/\$
116		df-ioo 11641	. . . . . . . . . . . . . . 15 $/\$
117		xrltnle 9703	. . . . . . . . . . . . . . 15 $/\$
118		xrlelttr 11455	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
119		xrlttr 11441	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
120	115, 116, 117, 116, 118, 119	ixxun 11653	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
121	107, 108, 110, 112, 114, 120	syl32anc 1273	. . . . . . . . . . . . 13 $/\$ $/\$
122		uncom 3611	. . . . . . . . . . . . 13
123		ioomax 11711	. . . . . . . . . . . . 13
124	121, 122, 123	3eqtr3g 2487	. . . . . . . . . . . 12 $/\$ $/\$
125		ioossre 11698	. . . . . . . . . . . . 13
126		incom 3656	. . . . . . . . . . . . . 14
127	115, 116, 117	ixxdisj 11652	. . . . . . . . . . . . . . . 16 $/\$ $/\$
128	64, 109, 127	mp3an13 1352	. . . . . . . . . . . . . . 15
129	108, 128	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$
130	126, 129	syl5eq 2476	. . . . . . . . . . . . 13 $/\$ $/\$
131		uneqdifeq 3885	. . . . . . . . . . . . 13 $/\$ $\$
132	125, 130, 131	sylancr 668	. . . . . . . . . . . 12 $/\$ $/\$ $\$
133	124, 132	mpbid 214	. . . . . . . . . . 11 $/\$ $/\$ $\$
134	133	imaeq2d 5185	. . . . . . . . . 10 $/\$ $/\$ $\$
135	106, 134	eqtr3d 2466	. . . . . . . . 9 $/\$ $/\$ $\$
136	42	ad2antrr 731	. . . . . . . . . 10 $/\$ $/\$
137	32	ad2antrr 731	. . . . . . . . . . 11 $/\$ $/\$
138		oveq1 6310	. . . . . . . . . . . . . 14
139	138	imaeq2d 5185	. . . . . . . . . . . . 13
140	139	eleq1d 2492	. . . . . . . . . . . 12
141	140	rspcv 3179	. . . . . . . . . . 11
142	56, 137, 141	sylc 63	. . . . . . . . . 10 $/\$ $/\$
143		difmbl 22488	. . . . . . . . . 10 $/\$ $\$
144	136, 142, 143	syl2anc 666	. . . . . . . . 9 $/\$ $/\$ $\$
145	135, 144	eqeltrrd 2512	. . . . . . . 8 $/\$ $/\$
146	145	ralrimiva 2840	. . . . . . 7 $/\$
147		iunmbl 22498	. . . . . . 7
148	146, 147	syl 17	. . . . . 6 $/\$
149	101, 148	eqeltrrd 2512	. . . . 5 $/\$
150	149	ralrimiva 2840	. . . 4
151		oveq2 6311	. . . . . . 7
152	151	imaeq2d 5185	. . . . . 6
153	152	eleq1d 2492	. . . . 5
154	153	cbvralv 3056	. . . 4
155	150, 154	sylib 200	. . 3
156	155	r19.21bi 2795	. 2 $/\$
157	1, 43, 31, 156	ismbf2d 22589	1 MblFn

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 188 $/\$ wa 371 $/\$ w3a 983

wceq 1438

wcel 1869

wral 2776

wrex 2777 $\$ cdif 3434

cun 3435

cin 3436

wss 3437

c0 3762

ciun 4297 class class class wbr 4421

ccnv 4850

cdm 4851

cima 4854

wfun 5593

wf 5595 (class class class)co 6303

cr 9540

cc0 9541

c1 9542

cpnf 9674

cmnf 9675

cxr 9676

clt 9677

cle 9678

cmin 9862

cneg 9863

cdiv 10271

cn 10611

crp 11304

cioo 11637

cioc 11638

cvol 22407 MblFncmbf 22564

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1666 ax-4 1679 ax-5 1749 ax-6 1795 ax-7 1840 ax-8 1871 ax-9 1873 ax-10 1888 ax-11 1893 ax-12 1906 ax-13 2054 ax-ext 2401 ax-rep 4534 ax-sep 4544 ax-nul 4553 ax-pow 4600 ax-pr 4658 ax-un 6595 ax-inf2 8150 ax-cc 8867 ax-cnex 9597 ax-resscn 9598 ax-1cn 9599 ax-icn 9600 ax-addcl 9601 ax-addrcl 9602 ax-mulcl 9603 ax-mulrcl 9604 ax-mulcom 9605 ax-addass 9606 ax-mulass 9607 ax-distr 9608 ax-i2m1 9609 ax-1ne0 9610 ax-1rid 9611 ax-rnegex 9612 ax-rrecex 9613 ax-cnre 9614 ax-pre-lttri 9615 ax-pre-lttrn 9616 ax-pre-ltadd 9617 ax-pre-mulgt0 9618 ax-pre-sup 9619

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 984 df-3an 985 df-tru 1441 df-fal 1444 df-ex 1661 df-nf 1665 df-sb 1788 df-eu 2270 df-mo 2271 df-clab 2409 df-cleq 2415 df-clel 2418 df-nfc 2573 df-ne 2621 df-nel 2622 df-ral 2781 df-rex 2782 df-reu 2783 df-rmo 2784 df-rab 2785 df-v 3084 df-sbc 3301 df-csb 3397 df-dif 3440 df-un 3442 df-in 3444 df-ss 3451 df-pss 3453 df-nul 3763 df-if 3911 df-pw 3982 df-sn 3998 df-pr 4000 df-tp 4002 df-op 4004 df-uni 4218 df-int 4254 df-iun 4299 df-disj 4393 df-br 4422 df-opab 4481 df-mpt 4482 df-tr 4517 df-eprel 4762 df-id 4766 df-po 4772 df-so 4773 df-fr 4810 df-se 4811 df-we 4812 df-xp 4857 df-rel 4858 df-cnv 4859 df-co 4860 df-dm 4861 df-rn 4862 df-res 4863 df-ima 4864 df-pred 5397 df-ord 5443 df-on 5444 df-lim 5445 df-suc 5446 df-iota 5563 df-fun 5601 df-fn 5602 df-f 5603 df-f1 5604 df-fo 5605 df-f1o 5606 df-fv 5607 df-isom 5608 df-riota 6265 df-ov 6306 df-oprab 6307 df-mpt2 6308 df-of 6543 df-om 6705 df-1st 6805 df-2nd 6806 df-wrecs 7034 df-recs 7096 df-rdg 7134 df-1o 7188 df-2o 7189 df-oadd 7192 df-er 7369 df-map 7480 df-pm 7481 df-en 7576 df-dom 7577 df-sdom 7578 df-fin 7579 df-sup 7960 df-inf 7961 df-oi 8029 df-card 8376 df-cda 8600 df-pnf 9679 df-mnf 9680 df-xr 9681 df-ltxr 9682 df-le 9683 df-sub 9864 df-neg 9865 df-div 10272 df-nn 10612 df-2 10670 df-3 10671 df-n0 10872 df-z 10940 df-uz 11162 df-q 11267 df-rp 11305 df-xadd 11412 df-ioo 11641 df-ioc 11642 df-ico 11643 df-icc 11644 df-fz 11787 df-fzo 11918 df-fl 12029 df-seq 12215 df-exp 12274 df-hash 12517 df-cj 13156 df-re 13157 df-im 13158 df-sqrt 13292 df-abs 13293 df-clim 13545 df-rlim 13546 df-sum 13746 df-xmet 18956 df-met 18957 df-ovol 22408 df-vol 22410 df-mbf 22569

This theorem is referenced by: mbfaddlem 22608 mbfsup 22612

W3C validator