ismbf3d - Metamath Proof Explorer

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

Theorem ismbf3d 22610

Description: Simplified form of ismbfd 22596. (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 6012	. . . 4
3	1, 2	syl 17	. . 3
4		imaiun 6150	. . . . 5
5		ioossre 11696	. . . . . . . . 9
6	5	rgenw 2749	. . . . . . . 8
7		iunss 4319	. . . . . . . 8
8	6, 7	mpbir 213	. . . . . . 7
9		renegcl 9937	. . . . . . . . . . 11
10		arch 10866	. . . . . . . . . . 11
11	9, 10	syl 17	. . . . . . . . . 10
12		simpl 459	. . . . . . . . . . . . 13 $/\$
13	12	biantrurd 511	. . . . . . . . . . . 12 $/\$ $/\$
14		nnre 10616	. . . . . . . . . . . . 13
15		ltnegcon1 10115	. . . . . . . . . . . . 13 $/\$
16	14, 15	sylan2 477	. . . . . . . . . . . 12 $/\$
17	14	adantl 468	. . . . . . . . . . . . . . 15 $/\$
18	17	renegcld 10046	. . . . . . . . . . . . . 14 $/\$
19	18	rexrd 9690	. . . . . . . . . . . . 13 $/\$
20		elioopnf 11728	. . . . . . . . . . . . 13 $/\$
21	19, 20	syl 17	. . . . . . . . . . . 12 $/\$ $/\$
22	13, 16, 21	3bitr4d 289	. . . . . . . . . . 11 $/\$
23	22	rexbidva 2898	. . . . . . . . . 10
24	11, 23	mpbid 214	. . . . . . . . 9
25		eliun 4283	. . . . . . . . 9
26	24, 25	sylibr 216	. . . . . . . 8
27	26	ssriv 3436	. . . . . . 7
28	8, 27	eqssi 3448	. . . . . 6
29	28	imaeq2i 5166	. . . . 5
30	4, 29	eqtr3i 2475	. . . 4
31		ismbf3d.2	. . . . . . . 8 $/\$
32	31	ralrimiva 2802	. . . . . . 7
33	14	renegcld 10046	. . . . . . 7
34		oveq1 6297	. . . . . . . . . 10
35	34	imaeq2d 5168	. . . . . . . . 9
36	35	eleq1d 2513	. . . . . . . 8
37	36	rspccva 3149	. . . . . . 7 $/\$
38	32, 33, 37	syl2an 480	. . . . . 6 $/\$
39	38	ralrimiva 2802	. . . . 5
40		iunmbl 22506	. . . . 5
41	39, 40	syl 17	. . . 4
42	30, 41	syl5eqelr 2534	. . 3
43	3, 42	eqeltrrd 2530	. 2
44		imaiun 6150	. . . . . . 7
45		eliun 4283	. . . . . . . . . 10
46		3simpb 1006	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
47		simplr 762	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
48		nnrp 11311	. . . . . . . . . . . . . . . . . . . . . 22
49	48	ad2antrl 734	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
50	49	rpreccld 11351	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
51	47, 50	ltsubrpd 11370	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
52		simprr 766	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
53		simpr 463	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
54		nnrecre 10646	. . . . . . . . . . . . . . . . . . . . . 22
55		resubcl 9938	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
56	53, 54, 55	syl2an 480	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
57	56	adantrr 723	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
58		lelttr 9724	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
59	52, 57, 47, 58	syl3anc 1268	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
60	51, 59	mpan2d 680	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
61	60	anassrs 654	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
62	61	imdistanda 699	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
63	46, 62	syl5 33	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
64		mnfxr 11414	. . . . . . . . . . . . . . . 16
65		elioc2 11697	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
66	64, 56, 65	sylancr 669	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
67		rexr 9686	. . . . . . . . . . . . . . . . . 18
68	67	adantl 468	. . . . . . . . . . . . . . . . 17 $/\$
69		elioomnf 11729	. . . . . . . . . . . . . . . . 17 $/\$
70	68, 69	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$
71	70	adantr 467	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
72	63, 66, 71	3imtr4d 272	. . . . . . . . . . . . . 14 $/\$ $/\$
73	72	rexlimdva 2879	. . . . . . . . . . . . 13 $/\$
74	73, 70	sylibd 218	. . . . . . . . . . . 12 $/\$ $/\$
75		simprl 764	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
76	75	adantr 467	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
77		mnflt 11425	. . . . . . . . . . . . . . . 16
78	76, 77	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
79	56	ad2ant2r 753	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
80	54	ad2antrl 734	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
81		simplr 762	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
82	81	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
83		simprr 766	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
84	80, 82, 76, 83	ltsub13d 10219	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
85	76, 79, 84	ltled 9783	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
86	66	ad2ant2r 753	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
87	76, 78, 85, 86	mpbir3and 1191	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
88	81, 75	resubcld 10047	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
89		simprr 766	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
90	75, 81	posdifd 10200	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
91	89, 90	mpbid 214	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
92		nnrecl 10867	. . . . . . . . . . . . . . 15 $/\$
93	88, 91, 92	syl2anc 667	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
94	87, 93	reximddv 2863	. . . . . . . . . . . . 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 2449	. . . . . . . 8 $/\$
100	99	imaeq2d 5168	. . . . . . 7 $/\$
101	44, 100	syl5eqr 2499	. . . . . 6 $/\$
102	1	ad2antrr 732	. . . . . . . . . . 11 $/\$ $/\$
103		ffun 5731	. . . . . . . . . . 11
104		funcnvcnv 5641	. . . . . . . . . . 11
105		imadif 5658	. . . . . . . . . . 11 $\$ $\$
106	102, 103, 104, 105	4syl 19	. . . . . . . . . 10 $/\$ $/\$ $\$ $\$
107	64	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
108	56	rexrd 9690	. . . . . . . . . . . . . 14 $/\$ $/\$
109		pnfxr 11412	. . . . . . . . . . . . . . 15
110	109	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
111		mnflt 11425	. . . . . . . . . . . . . . 15
112	56, 111	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$
113		ltpnf 11422	. . . . . . . . . . . . . . 15
114	56, 113	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$
115		df-ioc 11640	. . . . . . . . . . . . . . 15 $/\$
116		df-ioo 11639	. . . . . . . . . . . . . . 15 $/\$
117		xrltnle 9701	. . . . . . . . . . . . . . 15 $/\$
118		xrlelttr 11453	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
119		xrlttr 11439	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
120	115, 116, 117, 116, 118, 119	ixxun 11651	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
121	107, 108, 110, 112, 114, 120	syl32anc 1276	. . . . . . . . . . . . 13 $/\$ $/\$
122		uncom 3578	. . . . . . . . . . . . 13
123		ioomax 11709	. . . . . . . . . . . . 13
124	121, 122, 123	3eqtr3g 2508	. . . . . . . . . . . 12 $/\$ $/\$
125		ioossre 11696	. . . . . . . . . . . . 13
126		incom 3625	. . . . . . . . . . . . . 14
127	115, 116, 117	ixxdisj 11650	. . . . . . . . . . . . . . . 16 $/\$ $/\$
128	64, 109, 127	mp3an13 1355	. . . . . . . . . . . . . . 15
129	108, 128	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$
130	126, 129	syl5eq 2497	. . . . . . . . . . . . 13 $/\$ $/\$
131		uneqdifeq 3856	. . . . . . . . . . . . 13 $/\$ $\$
132	125, 130, 131	sylancr 669	. . . . . . . . . . . 12 $/\$ $/\$ $\$
133	124, 132	mpbid 214	. . . . . . . . . . 11 $/\$ $/\$ $\$
134	133	imaeq2d 5168	. . . . . . . . . 10 $/\$ $/\$ $\$
135	106, 134	eqtr3d 2487	. . . . . . . . 9 $/\$ $/\$ $\$
136	42	ad2antrr 732	. . . . . . . . . 10 $/\$ $/\$
137	32	ad2antrr 732	. . . . . . . . . . 11 $/\$ $/\$
138		oveq1 6297	. . . . . . . . . . . . . 14
139	138	imaeq2d 5168	. . . . . . . . . . . . 13
140	139	eleq1d 2513	. . . . . . . . . . . 12
141	140	rspcv 3146	. . . . . . . . . . 11
142	56, 137, 141	sylc 62	. . . . . . . . . 10 $/\$ $/\$
143		difmbl 22496	. . . . . . . . . 10 $/\$ $\$
144	136, 142, 143	syl2anc 667	. . . . . . . . 9 $/\$ $/\$ $\$
145	135, 144	eqeltrrd 2530	. . . . . . . 8 $/\$ $/\$
146	145	ralrimiva 2802	. . . . . . 7 $/\$
147		iunmbl 22506	. . . . . . 7
148	146, 147	syl 17	. . . . . 6 $/\$
149	101, 148	eqeltrrd 2530	. . . . 5 $/\$
150	149	ralrimiva 2802	. . . 4
151		oveq2 6298	. . . . . . 7
152	151	imaeq2d 5168	. . . . . 6
153	152	eleq1d 2513	. . . . 5
154	153	cbvralv 3019	. . . 4
155	150, 154	sylib 200	. . 3
156	155	r19.21bi 2757	. 2 $/\$
157	1, 43, 31, 156	ismbf2d 22597	1 MblFn

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1444

wcel 1887

wral 2737

wrex 2738 $\$ cdif 3401

cun 3402

cin 3403

wss 3404

c0 3731

ciun 4278 class class class wbr 4402

ccnv 4833

cdm 4834

cima 4837

wfun 5576

wf 5578 (class class class)co 6290

cr 9538

cc0 9539

c1 9540

cpnf 9672

cmnf 9673

cxr 9674

clt 9675

cle 9676

cmin 9860

cneg 9861

cdiv 10269

cn 10609

crp 11302

cioo 11635

cioc 11636

cvol 22415 MblFncmbf 22572

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-rep 4515 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-inf2 8146 ax-cc 8865 ax-cnex 9595 ax-resscn 9596 ax-1cn 9597 ax-icn 9598 ax-addcl 9599 ax-addrcl 9600 ax-mulcl 9601 ax-mulrcl 9602 ax-mulcom 9603 ax-addass 9604 ax-mulass 9605 ax-distr 9606 ax-i2m1 9607 ax-1ne0 9608 ax-1rid 9609 ax-rnegex 9610 ax-rrecex 9611 ax-cnre 9612 ax-pre-lttri 9613 ax-pre-lttrn 9614 ax-pre-ltadd 9615 ax-pre-mulgt0 9616 ax-pre-sup 9617

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-fal 1450 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-reu 2744 df-rmo 2745 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-tp 3973 df-op 3975 df-uni 4199 df-int 4235 df-iun 4280 df-disj 4374 df-br 4403 df-opab 4462 df-mpt 4463 df-tr 4498 df-eprel 4745 df-id 4749 df-po 4755 df-so 4756 df-fr 4793 df-se 4794 df-we 4795 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-pred 5380 df-ord 5426 df-on 5427 df-lim 5428 df-suc 5429 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-isom 5591 df-riota 6252 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-of 6531 df-om 6693 df-1st 6793 df-2nd 6794 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-1o 7182 df-2o 7183 df-oadd 7186 df-er 7363 df-map 7474 df-pm 7475 df-en 7570 df-dom 7571 df-sdom 7572 df-fin 7573 df-sup 7956 df-inf 7957 df-oi 8025 df-card 8373 df-cda 8598 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 df-sub 9862 df-neg 9863 df-div 10270 df-nn 10610 df-2 10668 df-3 10669 df-n0 10870 df-z 10938 df-uz 11160 df-q 11265 df-rp 11303 df-xadd 11410 df-ioo 11639 df-ioc 11640 df-ico 11641 df-icc 11642 df-fz 11785 df-fzo 11916 df-fl 12028 df-seq 12214 df-exp 12273 df-hash 12516 df-cj 13162 df-re 13163 df-im 13164 df-sqrt 13298 df-abs 13299 df-clim 13552 df-rlim 13553 df-sum 13753 df-xmet 18963 df-met 18964 df-ovol 22416 df-vol 22418 df-mbf 22577

This theorem is referenced by: mbfaddlem 22616 mbfsup 22620

W3C validator