voliunlem3 - Metamath Proof Explorer

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

Theorem voliunlem3 22088

Description: Lemma for voliun 22090. (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 22087	. . 3
5		mblvol 22067	. . 3
6	4, 5	syl 16	. 2
7		eqid 2457	. . . . 5
8		eqid 2457	. . . . 5
9	1	ffvelrnda 6032	. . . . . 6 $/\$
10		mblss 22068	. . . . . 6
11	9, 10	syl 16	. . . . 5 $/\$
12		mblvol 22067	. . . . . . 7
13	9, 12	syl 16	. . . . . 6 $/\$
14		voliunlem3.4	. . . . . . 7
15		fveq2 5872	. . . . . . . . . 10
16	15	fveq2d 5876	. . . . . . . . 9
17	16	eleq1d 2526	. . . . . . . 8
18	17	rspccva 3209	. . . . . . 7 $/\$
19	14, 18	sylan 471	. . . . . 6 $/\$
20	13, 19	eqeltrrd 2546	. . . . 5 $/\$
21	7, 8, 11, 20	ovoliun 22042	. . . 4
22		ffn 5737	. . . . . . 7
23	1, 22	syl 16	. . . . . 6
24		fniunfv 6160	. . . . . 6
25	23, 24	syl 16	. . . . 5
26	25	fveq2d 5876	. . . 4
27		voliunlem3.1	. . . . . . 7
28		voliunlem3.2	. . . . . . . . 9
29	13	mpteq2dva 4543	. . . . . . . . 9
30	28, 29	syl5eq 2510	. . . . . . . 8
31	30	seqeq3d 12118	. . . . . . 7
32	27, 31	syl5req 2511	. . . . . 6
33	32	rneqd 5240	. . . . 5
34	33	supeq1d 7923	. . . 4
35	21, 26, 34	3brtr3d 4485	. . 3
36		frn 5743	. . . . . . . . . . . . 13
37	1, 36	syl 16	. . . . . . . . . . . 12
38		mblss 22068	. . . . . . . . . . . . . 14
39		reex 9600	. . . . . . . . . . . . . . 15
40	39	elpw2 4620	. . . . . . . . . . . . . 14
41	38, 40	sylibr 212	. . . . . . . . . . . . 13
42	41	ssriv 3503	. . . . . . . . . . . 12
43	37, 42	syl6ss 3511	. . . . . . . . . . 11
44		sspwuni 4421	. . . . . . . . . . 11
45	43, 44	sylib 196	. . . . . . . . . 10
46		ovolcl 22015	. . . . . . . . . 10
47	45, 46	syl 16	. . . . . . . . 9
48		ovolge0 22018	. . . . . . . . . 10
49	45, 48	syl 16	. . . . . . . . 9
50		mnflt0 11359	. . . . . . . . . 10
51		mnfxr 11348	. . . . . . . . . . 11
52		0xr 9657	. . . . . . . . . . 11
53		xrltletr 11385	. . . . . . . . . . 11 $/\$ $/\$ $/\$
54	51, 52, 53	mp3an12 1314	. . . . . . . . . 10 $/\$
55	50, 54	mpani 676	. . . . . . . . 9
56	47, 49, 55	sylc 60	. . . . . . . 8
57		xrrebnd 11394	. . . . . . . . . 10 $/\$
58	47, 57	syl 16	. . . . . . . . 9 $/\$
59	39	elpw2 4620	. . . . . . . . . . . 12
60	45, 59	sylibr 212	. . . . . . . . . . 11
61		simpl 457	. . . . . . . . . . . . . . 15 $/\$
62	61	sseq1d 3526	. . . . . . . . . . . . . 14 $/\$
63	61	fveq2d 5876	. . . . . . . . . . . . . . . 16 $/\$
64	63	eleq1d 2526	. . . . . . . . . . . . . . 15 $/\$
65		simpll 753	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
66	65	ineq1d 3695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
67		fnfvelrn 6029	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
68	23, 67	sylan 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
69		elssuni 4281	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
70	68, 69	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
71	70	adantll 713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
72		sseqin2 3713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
73	71, 72	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
74	66, 73	eqtrd 2498	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
75	74	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
76	13	adantll 713	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
77	75, 76	eqtr4d 2501	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
78	77	mpteq2dva 4543	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
79	78	adantrr 716	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
80	79, 3, 28	3eqtr4g 2523	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
81	80	seqeq3d 12118	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
82	81, 27	syl6eqr 2516	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
83	82	fveq1d 5874	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
84		difeq1 3611	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$
85		difid 3899	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
86	84, 85	syl6eq 2514	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
87	86	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . 22 $\$
88		ovol0 22030	. . . . . . . . . . . . . . . . . . . . . 22
89	87, 88	syl6eq 2514	. . . . . . . . . . . . . . . . . . . . 21 $\$
90	89	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$
91	83, 90	oveq12d 6314	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $\$
92		nnuz 11141	. . . . . . . . . . . . . . . . . . . . . . . . 25
93		1zzd 10916	. . . . . . . . . . . . . . . . . . . . . . . . 25
94		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
95	94	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
96		fvex 5882	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
97	95, 28, 96	fvmpt 5956	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
98	97	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
99		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
100	99	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
101	100	eleq1d 2526	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
102	101	rspccva 3209	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
103	14, 102	sylan 471	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
104	98, 103	eqeltrd 2545	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
105	92, 93, 104	serfre 12139	. . . . . . . . . . . . . . . . . . . . . . . 24
106	27	feq1i 5729	. . . . . . . . . . . . . . . . . . . . . . . 24
107	105, 106	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . 23
108	107	ffvelrnda 6032	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
109	108	adantl 466	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
110	109	recnd 9639	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
111	110	addid1d 9797	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
112	91, 111	eqtrd 2498	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$
113		fveq2 5872	. . . . . . . . . . . . . . . . . . 19
114	113	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
115	112, 114	breq12d 4469	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$
116	115	expr 615	. . . . . . . . . . . . . . . 16 $/\$ $\$
117	116	pm5.74d 247	. . . . . . . . . . . . . . 15 $/\$ $\$
118	64, 117	imbi12d 320	. . . . . . . . . . . . . 14 $/\$ $\$
119	62, 118	imbi12d 320	. . . . . . . . . . . . 13 $/\$ $\$
120	119	pm5.74da 687	. . . . . . . . . . . 12 $\$
121	1	3ad2ant1 1017	. . . . . . . . . . . . . 14 $/\$ $/\$
122	2	3ad2ant1 1017	. . . . . . . . . . . . . 14 $/\$ $/\$ Disj
123		simp2 997	. . . . . . . . . . . . . 14 $/\$ $/\$
124		simp3 998	. . . . . . . . . . . . . 14 $/\$ $/\$
125	121, 122, 3, 123, 124	voliunlem1 22086	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
126	125	3exp1 1212	. . . . . . . . . . . 12 $\$
127	120, 126	vtoclg 3167	. . . . . . . . . . 11
128	60, 127	mpcom 36	. . . . . . . . . 10
129	45, 128	mpd 15	. . . . . . . . 9
130	58, 129	sylbird 235	. . . . . . . 8 $/\$
131	56, 130	mpand 675	. . . . . . 7
132		nltpnft 11392	. . . . . . . . 9
133	47, 132	syl 16	. . . . . . . 8
134		rexr 9656	. . . . . . . . . . 11
135		pnfge 11364	. . . . . . . . . . 11
136	108, 134, 135	3syl 20	. . . . . . . . . 10 $/\$
137	136	ex 434	. . . . . . . . 9
138		breq2 4460	. . . . . . . . . 10
139	138	imbi2d 316	. . . . . . . . 9
140	137, 139	syl5ibrcom 222	. . . . . . . 8
141	133, 140	sylbird 235	. . . . . . 7
142	131, 141	pm2.61d 158	. . . . . 6
143	142	ralrimiv 2869	. . . . 5
144		ffn 5737	. . . . . . 7
145	107, 144	syl 16	. . . . . 6
146		breq1 4459	. . . . . . 7
147	146	ralrn 6035	. . . . . 6
148	145, 147	syl 16	. . . . 5
149	143, 148	mpbird 232	. . . 4
150		frn 5743	. . . . . . 7
151	107, 150	syl 16	. . . . . 6
152		ressxr 9654	. . . . . 6
153	151, 152	syl6ss 3511	. . . . 5
154		supxrleub 11543	. . . . 5 $/\$
155	153, 47, 154	syl2anc 661	. . . 4
156	149, 155	mpbird 232	. . 3
157		supxrcl 11531	. . . . 5
158	153, 157	syl 16	. . . 4
159		xrletri3 11383	. . . 4 $/\$ $/\$
160	47, 158, 159	syl2anc 661	. . 3 $/\$
161	35, 156, 160	mpbir2and 922	. 2
162	6, 161	eqtrd 2498	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 973

wceq 1395

wcel 1819

wral 2807 $\$ cdif 3468

cin 3470

wss 3471

c0 3793

cpw 4015

cuni 4251

ciun 4332 Disj wdisj 4427 class class class wbr 4456

cmpt 4515

cdm 5008

crn 5009

wfn 5589

wf 5590

cfv 5594 (class class class)co 6296

csup 7918

cr 9508

cc0 9509

c1 9510

caddc 9512

cpnf 9642

cmnf 9643

cxr 9644

clt 9645

cle 9646

cn 10556

cseq 12110

covol 22000

cvol 22001

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-rep 4568 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-inf2 8075 ax-cc 8832 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586 ax-pre-sup 9587

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-fal 1401 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-int 4289 df-iun 4334 df-disj 4428 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-se 4848 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-isom 5603 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-of 6539 df-om 6700 df-1st 6799 df-2nd 6800 df-recs 7060 df-rdg 7094 df-1o 7148 df-2o 7149 df-oadd 7152 df-er 7329 df-map 7440 df-pm 7441 df-en 7536 df-dom 7537 df-sdom 7538 df-fin 7539 df-sup 7919 df-oi 7953 df-card 8337 df-cda 8565 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-div 10228 df-nn 10557 df-2 10615 df-3 10616 df-n0 10817 df-z 10886 df-uz 11107 df-q 11208 df-rp 11246 df-xadd 11344 df-ioo 11558 df-ico 11560 df-icc 11561 df-fz 11698 df-fzo 11822 df-fl 11932 df-seq 12111 df-exp 12170 df-hash 12409 df-cj 12944 df-re 12945 df-im 12946 df-sqrt 13080 df-abs 13081 df-clim 13323 df-rlim 13324 df-sum 13521 df-xmet 18539 df-met 18540 df-ovol 22002 df-vol 22003

This theorem is referenced by: voliun 22090

W3C validator