voliunlem3 - Metamath Proof Explorer

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

Theorem voliunlem3 22447

Description: Lemma for voliun 22449. (Contributed by Mario Carneiro, 20-Mar-2014.)

**Hypotheses**
Ref	Expression
voliunlem.3
voliunlem.5	Disj
voliunlem.6
voliunlem3.1
voliunlem3.2
voliunlem3.4

**Assertion**
Ref	Expression
voliunlem3

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

Proof of Theorem voliunlem3 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		voliunlem.3	. . . 4
2		voliunlem.5	. . . 4 Disj
3		voliunlem.6	. . . 4
4	1, 2, 3	voliunlem2 22446	. . 3
5		mblvol 22426	. . 3
6	4, 5	syl 17	. 2
7		eqid 2428	. . . . 5
8		eqid 2428	. . . . 5
9	1	ffvelrnda 5981	. . . . . 6 $/\$
10		mblss 22427	. . . . . 6
11	9, 10	syl 17	. . . . 5 $/\$
12		mblvol 22426	. . . . . . 7
13	9, 12	syl 17	. . . . . 6 $/\$
14		voliunlem3.4	. . . . . . 7
15		fveq2 5825	. . . . . . . . . 10
16	15	fveq2d 5829	. . . . . . . . 9
17	16	eleq1d 2490	. . . . . . . 8
18	17	rspccva 3124	. . . . . . 7 $/\$
19	14, 18	sylan 473	. . . . . 6 $/\$
20	13, 19	eqeltrrd 2507	. . . . 5 $/\$
21	7, 8, 11, 20	ovoliun 22400	. . . 4
22		ffn 5689	. . . . . . 7
23	1, 22	syl 17	. . . . . 6
24		fniunfv 6111	. . . . . 6
25	23, 24	syl 17	. . . . 5
26	25	fveq2d 5829	. . . 4
27		voliunlem3.1	. . . . . . 7
28		voliunlem3.2	. . . . . . . . 9
29	13	mpteq2dva 4453	. . . . . . . . 9
30	28, 29	syl5eq 2474	. . . . . . . 8
31	30	seqeq3d 12171	. . . . . . 7
32	27, 31	syl5req 2475	. . . . . 6
33	32	rneqd 5024	. . . . 5
34	33	supeq1d 7913	. . . 4
35	21, 26, 34	3brtr3d 4396	. . 3
36		frn 5695	. . . . . . . . . . . . 13
37	1, 36	syl 17	. . . . . . . . . . . 12
38		mblss 22427	. . . . . . . . . . . . . 14
39		reex 9581	. . . . . . . . . . . . . . 15
40	39	elpw2 4531	. . . . . . . . . . . . . 14
41	38, 40	sylibr 215	. . . . . . . . . . . . 13
42	41	ssriv 3411	. . . . . . . . . . . 12
43	37, 42	syl6ss 3419	. . . . . . . . . . 11
44		sspwuni 4331	. . . . . . . . . . 11
45	43, 44	sylib 199	. . . . . . . . . 10
46		ovolcl 22373	. . . . . . . . . 10
47	45, 46	syl 17	. . . . . . . . 9
48		ovolge0 22376	. . . . . . . . . 10
49	45, 48	syl 17	. . . . . . . . 9
50		mnflt0 11378	. . . . . . . . . 10
51		mnfxr 11365	. . . . . . . . . . 11
52		0xr 9638	. . . . . . . . . . 11
53		xrltletr 11405	. . . . . . . . . . 11 $/\$ $/\$ $/\$
54	51, 52, 53	mp3an12 1350	. . . . . . . . . 10 $/\$
55	50, 54	mpani 680	. . . . . . . . 9
56	47, 49, 55	sylc 62	. . . . . . . 8
57		xrrebnd 11414	. . . . . . . . . 10 $/\$
58	47, 57	syl 17	. . . . . . . . 9 $/\$
59	39	elpw2 4531	. . . . . . . . . . . 12
60	45, 59	sylibr 215	. . . . . . . . . . 11
61		simpl 458	. . . . . . . . . . . . . . 15 $/\$
62	61	sseq1d 3434	. . . . . . . . . . . . . 14 $/\$
63	61	fveq2d 5829	. . . . . . . . . . . . . . . 16 $/\$
64	63	eleq1d 2490	. . . . . . . . . . . . . . 15 $/\$
65		simpll 758	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
66	65	ineq1d 3606	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
67		fnfvelrn 5978	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
68	23, 67	sylan 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
69		elssuni 4191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
70	68, 69	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
71	70	adantll 718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
72		sseqin2 3624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
73	71, 72	sylib 199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
74	66, 73	eqtrd 2462	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
75	74	fveq2d 5829	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
76	13	adantll 718	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
77	75, 76	eqtr4d 2465	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
78	77	mpteq2dva 4453	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
79	78	adantrr 721	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
80	79, 3, 28	3eqtr4g 2487	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
81	80	seqeq3d 12171	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
82	81, 27	syl6eqr 2480	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
83	82	fveq1d 5827	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
84		difeq1 3519	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$
85		difid 3808	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
86	84, 85	syl6eq 2478	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
87	86	fveq2d 5829	. . . . . . . . . . . . . . . . . . . . . 22 $\$
88		ovol0 22388	. . . . . . . . . . . . . . . . . . . . . 22
89	87, 88	syl6eq 2478	. . . . . . . . . . . . . . . . . . . . 21 $\$
90	89	adantr 466	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$
91	83, 90	oveq12d 6267	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $\$
92		nnuz 11145	. . . . . . . . . . . . . . . . . . . . . . . . 25
93		1zzd 10919	. . . . . . . . . . . . . . . . . . . . . . . . 25
94		fveq2 5825	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
95	94	fveq2d 5829	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
96		fvex 5835	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
97	95, 28, 96	fvmpt 5908	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
98	97	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
99		fveq2 5825	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
100	99	fveq2d 5829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
101	100	eleq1d 2490	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
102	101	rspccva 3124	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
103	14, 102	sylan 473	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
104	98, 103	eqeltrd 2506	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
105	92, 93, 104	serfre 12192	. . . . . . . . . . . . . . . . . . . . . . . 24
106	27	feq1i 5681	. . . . . . . . . . . . . . . . . . . . . . . 24
107	105, 106	sylibr 215	. . . . . . . . . . . . . . . . . . . . . . 23
108	107	ffvelrnda 5981	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
109	108	adantl 467	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
110	109	recnd 9620	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
111	110	addid1d 9784	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
112	91, 111	eqtrd 2462	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$
113		fveq2 5825	. . . . . . . . . . . . . . . . . . 19
114	113	adantr 466	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
115	112, 114	breq12d 4379	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$
116	115	expr 618	. . . . . . . . . . . . . . . 16 $/\$ $\$
117	116	pm5.74d 250	. . . . . . . . . . . . . . 15 $/\$ $\$
118	64, 117	imbi12d 321	. . . . . . . . . . . . . 14 $/\$ $\$
119	62, 118	imbi12d 321	. . . . . . . . . . . . 13 $/\$ $\$
120	119	pm5.74da 691	. . . . . . . . . . . 12 $\$
121	1	3ad2ant1 1026	. . . . . . . . . . . . . 14 $/\$ $/\$
122	2	3ad2ant1 1026	. . . . . . . . . . . . . 14 $/\$ $/\$ Disj
123		simp2 1006	. . . . . . . . . . . . . 14 $/\$ $/\$
124		simp3 1007	. . . . . . . . . . . . . 14 $/\$ $/\$
125	121, 122, 3, 123, 124	voliunlem1 22445	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
126	125	3exp1 1221	. . . . . . . . . . . 12 $\$
127	120, 126	vtoclg 3082	. . . . . . . . . . 11
128	60, 127	mpcom 37	. . . . . . . . . 10
129	45, 128	mpd 15	. . . . . . . . 9
130	58, 129	sylbird 238	. . . . . . . 8 $/\$
131	56, 130	mpand 679	. . . . . . 7
132		nltpnft 11412	. . . . . . . . 9
133	47, 132	syl 17	. . . . . . . 8
134		rexr 9637	. . . . . . . . . . 11
135		pnfge 11383	. . . . . . . . . . 11
136	108, 134, 135	3syl 18	. . . . . . . . . 10 $/\$
137	136	ex 435	. . . . . . . . 9
138		breq2 4370	. . . . . . . . . 10
139	138	imbi2d 317	. . . . . . . . 9
140	137, 139	syl5ibrcom 225	. . . . . . . 8
141	133, 140	sylbird 238	. . . . . . 7
142	131, 141	pm2.61d 161	. . . . . 6
143	142	ralrimiv 2777	. . . . 5
144		ffn 5689	. . . . . . 7
145	107, 144	syl 17	. . . . . 6
146		breq1 4369	. . . . . . 7
147	146	ralrn 5984	. . . . . 6
148	145, 147	syl 17	. . . . 5
149	143, 148	mpbird 235	. . . 4
150		frn 5695	. . . . . . 7
151	107, 150	syl 17	. . . . . 6
152		ressxr 9635	. . . . . 6
153	151, 152	syl6ss 3419	. . . . 5
154		supxrleub 11563	. . . . 5 $/\$
155	153, 47, 154	syl2anc 665	. . . 4
156	149, 155	mpbird 235	. . 3
157		supxrcl 11551	. . . . 5
158	153, 157	syl 17	. . . 4
159		xrletri3 11402	. . . 4 $/\$ $/\$
160	47, 158, 159	syl2anc 665	. . 3 $/\$
161	35, 156, 160	mpbir2and 930	. 2
162	6, 161	eqtrd 2462	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 187 $/\$ wa 370 $/\$ w3a 982

wceq 1437

wcel 1872

wral 2714 $\$ cdif 3376

cin 3378

wss 3379

c0 3704

cpw 3924

cuni 4162

ciun 4242 Disj wdisj 4337 class class class wbr 4366

cmpt 4425

cdm 4796

crn 4797

wfn 5539

wf 5540

cfv 5544 (class class class)co 6249

csup 7907

cr 9489

cc0 9490

c1 9491

caddc 9493

cpnf 9623

cmnf 9624

cxr 9625

clt 9626

cle 9627

cn 10560

cseq 12163

covol 22355

cvol 22357

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1663 ax-4 1676 ax-5 1752 ax-6 1798 ax-7 1843 ax-8 1874 ax-9 1876 ax-10 1891 ax-11 1896 ax-12 1909 ax-13 2063 ax-ext 2408 ax-rep 4479 ax-sep 4489 ax-nul 4498 ax-pow 4545 ax-pr 4603 ax-un 6541 ax-inf2 8099 ax-cc 8816 ax-cnex 9546 ax-resscn 9547 ax-1cn 9548 ax-icn 9549 ax-addcl 9550 ax-addrcl 9551 ax-mulcl 9552 ax-mulrcl 9553 ax-mulcom 9554 ax-addass 9555 ax-mulass 9556 ax-distr 9557 ax-i2m1 9558 ax-1ne0 9559 ax-1rid 9560 ax-rnegex 9561 ax-rrecex 9562 ax-cnre 9563 ax-pre-lttri 9564 ax-pre-lttrn 9565 ax-pre-ltadd 9566 ax-pre-mulgt0 9567 ax-pre-sup 9568

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-fal 1443 df-ex 1658 df-nf 1662 df-sb 1791 df-eu 2280 df-mo 2281 df-clab 2415 df-cleq 2421 df-clel 2424 df-nfc 2558 df-ne 2601 df-nel 2602 df-ral 2719 df-rex 2720 df-reu 2721 df-rmo 2722 df-rab 2723 df-v 3024 df-sbc 3243 df-csb 3339 df-dif 3382 df-un 3384 df-in 3386 df-ss 3393 df-pss 3395 df-nul 3705 df-if 3855 df-pw 3926 df-sn 3942 df-pr 3944 df-tp 3946 df-op 3948 df-uni 4163 df-int 4199 df-iun 4244 df-disj 4338 df-br 4367 df-opab 4426 df-mpt 4427 df-tr 4462 df-eprel 4707 df-id 4711 df-po 4717 df-so 4718 df-fr 4755 df-se 4756 df-we 4757 df-xp 4802 df-rel 4803 df-cnv 4804 df-co 4805 df-dm 4806 df-rn 4807 df-res 4808 df-ima 4809 df-pred 5342 df-ord 5388 df-on 5389 df-lim 5390 df-suc 5391 df-iota 5508 df-fun 5546 df-fn 5547 df-f 5548 df-f1 5549 df-fo 5550 df-f1o 5551 df-fv 5552 df-isom 5553 df-riota 6211 df-ov 6252 df-oprab 6253 df-mpt2 6254 df-of 6489 df-om 6651 df-1st 6751 df-2nd 6752 df-wrecs 6983 df-recs 7045 df-rdg 7083 df-1o 7137 df-2o 7138 df-oadd 7141 df-er 7318 df-map 7429 df-pm 7430 df-en 7525 df-dom 7526 df-sdom 7527 df-fin 7528 df-sup 7909 df-inf 7910 df-oi 7978 df-card 8325 df-cda 8549 df-pnf 9628 df-mnf 9629 df-xr 9630 df-ltxr 9631 df-le 9632 df-sub 9813 df-neg 9814 df-div 10221 df-nn 10561 df-2 10619 df-3 10620 df-n0 10821 df-z 10889 df-uz 11111 df-q 11216 df-rp 11254 df-xadd 11361 df-ioo 11590 df-ico 11592 df-icc 11593 df-fz 11736 df-fzo 11867 df-fl 11978 df-seq 12164 df-exp 12223 df-hash 12466 df-cj 13106 df-re 13107 df-im 13108 df-sqrt 13242 df-abs 13243 df-clim 13495 df-rlim 13496 df-sum 13696 df-xmet 18906 df-met 18907 df-ovol 22358 df-vol 22360

This theorem is referenced by: voliun 22449

W3C validator