ismbf3d - Metamath Proof Explorer

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

Theorem ismbf3d 22353

Description: Simplified form of ismbfd 22339. (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 5997	. . . 4
3	1, 2	syl 17	. . 3
4		imaiun 6138	. . . . 5
5		ioossre 11640	. . . . . . . . 9
6	5	rgenw 2765	. . . . . . . 8
7		iunss 4312	. . . . . . . 8
8	6, 7	mpbir 209	. . . . . . 7
9		renegcl 9918	. . . . . . . . . . 11
10		arch 10833	. . . . . . . . . . 11
11	9, 10	syl 17	. . . . . . . . . 10
12		simpl 455	. . . . . . . . . . . . 13 $/\$
13	12	biantrurd 506	. . . . . . . . . . . 12 $/\$ $/\$
14		nnre 10583	. . . . . . . . . . . . 13
15		ltnegcon1 10094	. . . . . . . . . . . . 13 $/\$
16	14, 15	sylan2 472	. . . . . . . . . . . 12 $/\$
17	14	adantl 464	. . . . . . . . . . . . . . 15 $/\$
18	17	renegcld 10027	. . . . . . . . . . . . . 14 $/\$
19	18	rexrd 9673	. . . . . . . . . . . . 13 $/\$
20		elioopnf 11672	. . . . . . . . . . . . 13 $/\$
21	19, 20	syl 17	. . . . . . . . . . . 12 $/\$ $/\$
22	13, 16, 21	3bitr4d 285	. . . . . . . . . . 11 $/\$
23	22	rexbidva 2915	. . . . . . . . . 10
24	11, 23	mpbid 210	. . . . . . . . 9
25		eliun 4276	. . . . . . . . 9
26	24, 25	sylibr 212	. . . . . . . 8
27	26	ssriv 3446	. . . . . . 7
28	8, 27	eqssi 3458	. . . . . 6
29	28	imaeq2i 5155	. . . . 5
30	4, 29	eqtr3i 2433	. . . 4
31		ismbf3d.2	. . . . . . . 8 $/\$
32	31	ralrimiva 2818	. . . . . . 7
33	14	renegcld 10027	. . . . . . 7
34		oveq1 6285	. . . . . . . . . 10
35	34	imaeq2d 5157	. . . . . . . . 9
36	35	eleq1d 2471	. . . . . . . 8
37	36	rspccva 3159	. . . . . . 7 $/\$
38	32, 33, 37	syl2an 475	. . . . . 6 $/\$
39	38	ralrimiva 2818	. . . . 5
40		iunmbl 22255	. . . . 5
41	39, 40	syl 17	. . . 4
42	30, 41	syl5eqelr 2495	. . 3
43	3, 42	eqeltrrd 2491	. 2
44		imaiun 6138	. . . . . . 7
45		eliun 4276	. . . . . . . . . 10
46		3simpb 995	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
47		simplr 754	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
48		nnrp 11274	. . . . . . . . . . . . . . . . . . . . . 22
49	48	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
50	49	rpreccld 11314	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
51	47, 50	ltsubrpd 11332	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
52		simprr 758	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
53		simpr 459	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
54		nnrecre 10613	. . . . . . . . . . . . . . . . . . . . . 22
55		resubcl 9919	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
56	53, 54, 55	syl2an 475	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
57	56	adantrr 715	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
58		lelttr 9706	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
59	52, 57, 47, 58	syl3anc 1230	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
60	51, 59	mpan2d 672	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
61	60	anassrs 646	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
62	61	imdistanda 691	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
63	46, 62	syl5 30	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
64		mnfxr 11376	. . . . . . . . . . . . . . . 16
65		elioc2 11641	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
66	64, 56, 65	sylancr 661	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
67		rexr 9669	. . . . . . . . . . . . . . . . . 18
68	67	adantl 464	. . . . . . . . . . . . . . . . 17 $/\$
69		elioomnf 11673	. . . . . . . . . . . . . . . . 17 $/\$
70	68, 69	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$
71	70	adantr 463	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
72	63, 66, 71	3imtr4d 268	. . . . . . . . . . . . . 14 $/\$ $/\$
73	72	rexlimdva 2896	. . . . . . . . . . . . 13 $/\$
74	73, 70	sylibd 214	. . . . . . . . . . . 12 $/\$ $/\$
75		simprl 756	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
76	75	adantr 463	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
77		mnflt 11386	. . . . . . . . . . . . . . . 16
78	76, 77	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
79	56	ad2ant2r 745	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
80	54	ad2antrl 726	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
81		simplr 754	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
82	81	adantr 463	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
83		simprr 758	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
84	80, 82, 76, 83	ltsub13d 10198	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
85	76, 79, 84	ltled 9765	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
86	66	ad2ant2r 745	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
87	76, 78, 85, 86	mpbir3and 1180	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
88	81, 75	resubcld 10028	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
89		simprr 758	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
90	75, 81	posdifd 10179	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
91	89, 90	mpbid 210	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
92		nnrecl 10834	. . . . . . . . . . . . . . 15 $/\$
93	88, 91, 92	syl2anc 659	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
94	87, 93	reximddv 2880	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
95	94	ex 432	. . . . . . . . . . . 12 $/\$ $/\$
96	74, 95	impbid 190	. . . . . . . . . . 11 $/\$ $/\$
97	96, 70	bitr4d 256	. . . . . . . . . 10 $/\$
98	45, 97	syl5bb 257	. . . . . . . . 9 $/\$
99	98	eqrdv 2399	. . . . . . . 8 $/\$
100	99	imaeq2d 5157	. . . . . . 7 $/\$
101	44, 100	syl5eqr 2457	. . . . . 6 $/\$
102	1	ad2antrr 724	. . . . . . . . . . 11 $/\$ $/\$
103		ffun 5716	. . . . . . . . . . 11
104		funcnvcnv 5627	. . . . . . . . . . 11
105		imadif 5644	. . . . . . . . . . 11 $\$ $\$
106	102, 103, 104, 105	4syl 19	. . . . . . . . . 10 $/\$ $/\$ $\$ $\$
107	64	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
108	56	rexrd 9673	. . . . . . . . . . . . . 14 $/\$ $/\$
109		pnfxr 11374	. . . . . . . . . . . . . . 15
110	109	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
111		mnflt 11386	. . . . . . . . . . . . . . 15
112	56, 111	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$
113		ltpnf 11384	. . . . . . . . . . . . . . 15
114	56, 113	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$
115		df-ioc 11587	. . . . . . . . . . . . . . 15 $/\$
116		df-ioo 11586	. . . . . . . . . . . . . . 15 $/\$
117		xrltnle 9683	. . . . . . . . . . . . . . 15 $/\$
118		xrlelttr 11412	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
119		xrlttr 11399	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
120	115, 116, 117, 116, 118, 119	ixxun 11598	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
121	107, 108, 110, 112, 114, 120	syl32anc 1238	. . . . . . . . . . . . 13 $/\$ $/\$
122		uncom 3587	. . . . . . . . . . . . 13
123		ioomax 11653	. . . . . . . . . . . . 13
124	121, 122, 123	3eqtr3g 2466	. . . . . . . . . . . 12 $/\$ $/\$
125		ioossre 11640	. . . . . . . . . . . . 13
126		incom 3632	. . . . . . . . . . . . . 14
127	115, 116, 117	ixxdisj 11597	. . . . . . . . . . . . . . . 16 $/\$ $/\$
128	64, 109, 127	mp3an13 1317	. . . . . . . . . . . . . . 15
129	108, 128	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$
130	126, 129	syl5eq 2455	. . . . . . . . . . . . 13 $/\$ $/\$
131		uneqdifeq 3860	. . . . . . . . . . . . 13 $/\$ $\$
132	125, 130, 131	sylancr 661	. . . . . . . . . . . 12 $/\$ $/\$ $\$
133	124, 132	mpbid 210	. . . . . . . . . . 11 $/\$ $/\$ $\$
134	133	imaeq2d 5157	. . . . . . . . . 10 $/\$ $/\$ $\$
135	106, 134	eqtr3d 2445	. . . . . . . . 9 $/\$ $/\$ $\$
136	42	ad2antrr 724	. . . . . . . . . 10 $/\$ $/\$
137	32	ad2antrr 724	. . . . . . . . . . 11 $/\$ $/\$
138		oveq1 6285	. . . . . . . . . . . . . 14
139	138	imaeq2d 5157	. . . . . . . . . . . . 13
140	139	eleq1d 2471	. . . . . . . . . . . 12
141	140	rspcv 3156	. . . . . . . . . . 11
142	56, 137, 141	sylc 59	. . . . . . . . . 10 $/\$ $/\$
143		difmbl 22245	. . . . . . . . . 10 $/\$ $\$
144	136, 142, 143	syl2anc 659	. . . . . . . . 9 $/\$ $/\$ $\$
145	135, 144	eqeltrrd 2491	. . . . . . . 8 $/\$ $/\$
146	145	ralrimiva 2818	. . . . . . 7 $/\$
147		iunmbl 22255	. . . . . . 7
148	146, 147	syl 17	. . . . . 6 $/\$
149	101, 148	eqeltrrd 2491	. . . . 5 $/\$
150	149	ralrimiva 2818	. . . 4
151		oveq2 6286	. . . . . . 7
152	151	imaeq2d 5157	. . . . . 6
153	152	eleq1d 2471	. . . . 5
154	153	cbvralv 3034	. . . 4
155	150, 154	sylib 196	. . 3
156	155	r19.21bi 2773	. 2 $/\$
157	1, 43, 31, 156	ismbf2d 22340	1 MblFn

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 367 $/\$ w3a 974

wceq 1405

wcel 1842

wral 2754

wrex 2755 $\$ cdif 3411

cun 3412

cin 3413

wss 3414

c0 3738

ciun 4271 class class class wbr 4395

ccnv 4822

cdm 4823

cima 4826

wfun 5563

wf 5565 (class class class)co 6278

cr 9521

cc0 9522

c1 9523

cpnf 9655

cmnf 9656

cxr 9657

clt 9658

cle 9659

cmin 9841

cneg 9842

cdiv 10247

cn 10576

crp 11265

cioo 11582

cioc 11583

cvol 22167 MblFncmbf 22315

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1639 ax-4 1652 ax-5 1725 ax-6 1771 ax-7 1814 ax-8 1844 ax-9 1846 ax-10 1861 ax-11 1866 ax-12 1878 ax-13 2026 ax-ext 2380 ax-rep 4507 ax-sep 4517 ax-nul 4525 ax-pow 4572 ax-pr 4630 ax-un 6574 ax-inf2 8091 ax-cc 8847 ax-cnex 9578 ax-resscn 9579 ax-1cn 9580 ax-icn 9581 ax-addcl 9582 ax-addrcl 9583 ax-mulcl 9584 ax-mulrcl 9585 ax-mulcom 9586 ax-addass 9587 ax-mulass 9588 ax-distr 9589 ax-i2m1 9590 ax-1ne0 9591 ax-1rid 9592 ax-rnegex 9593 ax-rrecex 9594 ax-cnre 9595 ax-pre-lttri 9596 ax-pre-lttrn 9597 ax-pre-ltadd 9598 ax-pre-mulgt0 9599 ax-pre-sup 9600

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 975 df-3an 976 df-tru 1408 df-fal 1411 df-ex 1634 df-nf 1638 df-sb 1764 df-eu 2242 df-mo 2243 df-clab 2388 df-cleq 2394 df-clel 2397 df-nfc 2552 df-ne 2600 df-nel 2601 df-ral 2759 df-rex 2760 df-reu 2761 df-rmo 2762 df-rab 2763 df-v 3061 df-sbc 3278 df-csb 3374 df-dif 3417 df-un 3419 df-in 3421 df-ss 3428 df-pss 3430 df-nul 3739 df-if 3886 df-pw 3957 df-sn 3973 df-pr 3975 df-tp 3977 df-op 3979 df-uni 4192 df-int 4228 df-iun 4273 df-disj 4367 df-br 4396 df-opab 4454 df-mpt 4455 df-tr 4490 df-eprel 4734 df-id 4738 df-po 4744 df-so 4745 df-fr 4782 df-se 4783 df-we 4784 df-xp 4829 df-rel 4830 df-cnv 4831 df-co 4832 df-dm 4833 df-rn 4834 df-res 4835 df-ima 4836 df-pred 5367 df-ord 5413 df-on 5414 df-lim 5415 df-suc 5416 df-iota 5533 df-fun 5571 df-fn 5572 df-f 5573 df-f1 5574 df-fo 5575 df-f1o 5576 df-fv 5577 df-isom 5578 df-riota 6240 df-ov 6281 df-oprab 6282 df-mpt2 6283 df-of 6521 df-om 6684 df-1st 6784 df-2nd 6785 df-wrecs 7013 df-recs 7075 df-rdg 7113 df-1o 7167 df-2o 7168 df-oadd 7171 df-er 7348 df-map 7459 df-pm 7460 df-en 7555 df-dom 7556 df-sdom 7557 df-fin 7558 df-sup 7935 df-oi 7969 df-card 8352 df-cda 8580 df-pnf 9660 df-mnf 9661 df-xr 9662 df-ltxr 9663 df-le 9664 df-sub 9843 df-neg 9844 df-div 10248 df-nn 10577 df-2 10635 df-3 10636 df-n0 10837 df-z 10906 df-uz 11128 df-q 11228 df-rp 11266 df-xadd 11372 df-ioo 11586 df-ioc 11587 df-ico 11588 df-icc 11589 df-fz 11727 df-fzo 11855 df-fl 11966 df-seq 12152 df-exp 12211 df-hash 12453 df-cj 13081 df-re 13082 df-im 13083 df-sqrt 13217 df-abs 13218 df-clim 13460 df-rlim 13461 df-sum 13658 df-xmet 18732 df-met 18733 df-ovol 22168 df-vol 22169 df-mbf 22320

This theorem is referenced by: mbfaddlem 22359 mbfsup 22363

W3C validator