ovnsubaddlem1 - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > ovnsubaddlem1		Structured version Visualization version Unicode version

Theorem ovnsubaddlem1 40784

Description: The Lebesgue outer measure is subadditive. Proposition 115D (a)(iv) of [Fremlin1] p. 31 . (Contributed by Glauco Siliprandi, 11-Oct-2020.)

**Hypotheses**
Ref	Expression
ovnsubaddlem1.x
ovnsubaddlem1.n0
ovnsubaddlem1.a
ovnsubaddlem1.e
ovnsubaddlem1.z	$/\$ Σ^{^}
ovnsubaddlem1.c
ovnsubaddlem1.l
ovnsubaddlem1.d	Σ^{^} voln^*
ovnsubaddlem1.i	$/\$
ovnsubaddlem1.f
ovnsubaddlem1.g

**Assertion**
Ref	Expression
ovnsubaddlem1	voln^* Σ^{^} voln^*

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

Proof of Theorem ovnsubaddlem1 Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ovnsubaddlem1.x	. . . 4
2		ovnsubaddlem1.a	. . . . . . . . 9
3	2	adantr 481	. . . . . . . 8 $/\$
4		simpr 477	. . . . . . . 8 $/\$
5	3, 4	ffvelrnd 6360	. . . . . . 7 $/\$
6		elpwi 4168	. . . . . . 7
7	5, 6	syl 17	. . . . . 6 $/\$
8	7	ralrimiva 2966	. . . . 5
9		iunss 4561	. . . . 5
10	8, 9	sylibr 224	. . . 4
11	1, 10	ovnxrcl 40783	. . 3 voln^*
12		nfv 1843	. . . 4
13		nnex 11026	. . . . 5
14	13	a1i 11	. . . 4
15		icossicc 12260	. . . . 5
16		nfv 1843	. . . . . 6 $/\$
17		simpl 473	. . . . . . 7 $/\$
18	17, 1	syl 17	. . . . . 6 $/\$
19		ovnsubaddlem1.l	. . . . . 6
20		ovnsubaddlem1.f	. . . . . . . . . . . 12
21		f1of 6137	. . . . . . . . . . . 12
22	20, 21	syl 17	. . . . . . . . . . 11
23	22	adantr 481	. . . . . . . . . 10 $/\$
24		simpr 477	. . . . . . . . . 10 $/\$
25	23, 24	ffvelrnd 6360	. . . . . . . . 9 $/\$
26		xp1st 7198	. . . . . . . . 9
27	25, 26	syl 17	. . . . . . . 8 $/\$
28		xp2nd 7199	. . . . . . . . 9
29	25, 28	syl 17	. . . . . . . 8 $/\$
30		fvex 6201	. . . . . . . . 9
31		eleq1 2689	. . . . . . . . . . 11
32	31	3anbi3d 1405	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
33		fveq2 6191	. . . . . . . . . . 11
34	33	feq1d 6030	. . . . . . . . . 10
35	32, 34	imbi12d 334	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
36		fvex 6201	. . . . . . . . . 10
37		eleq1 2689	. . . . . . . . . . . 12
38	37	3anbi2d 1404	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
39		fveq2 6191	. . . . . . . . . . . . 13
40	39	fveq1d 6193	. . . . . . . . . . . 12
41	40	feq1d 6030	. . . . . . . . . . 11
42	38, 41	imbi12d 334	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
43		ovnsubaddlem1.c	. . . . . . . . . . . . . . . . . . . 20
44	43	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$
45		sseq1 3626	. . . . . . . . . . . . . . . . . . . . 21
46	45	rabbidv 3189	. . . . . . . . . . . . . . . . . . . 20
47	46	adantl 482	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
48		ovex 6678	. . . . . . . . . . . . . . . . . . . . 21
49	48	rabex 4813	. . . . . . . . . . . . . . . . . . . 20
50	49	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$
51	44, 47, 5, 50	fvmptd 6288	. . . . . . . . . . . . . . . . . 18 $/\$
52		ssrab2 3687	. . . . . . . . . . . . . . . . . . 19
53	52	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$
54	51, 53	eqsstrd 3639	. . . . . . . . . . . . . . . . 17 $/\$
55		ovnsubaddlem1.d	. . . . . . . . . . . . . . . . . . . . . 22 Σ^{^} voln^*
56	55	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 $/\$ Σ^{^} voln^*
57		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . 26
58	57	eleq2d 2687	. . . . . . . . . . . . . . . . . . . . . . . . 25
59		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 voln^* voln^*
60	59	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . 26 voln^* voln^*
61	60	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . . . . 25 Σ^{^} voln^* Σ^{^} voln^*
62	58, 61	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ Σ^{^} voln^* $/\$ Σ^{^} voln^*
63	62	rabbidva2 3186	. . . . . . . . . . . . . . . . . . . . . . 23 Σ^{^} voln^* Σ^{^} voln^*
64	63	mpteq2dv 4745	. . . . . . . . . . . . . . . . . . . . . 22 Σ^{^} voln^* Σ^{^} voln^*
65	64	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ Σ^{^} voln^* Σ^{^} voln^*
66		rpex 39562	. . . . . . . . . . . . . . . . . . . . . . 23
67	66	mptex 6486	. . . . . . . . . . . . . . . . . . . . . 22 Σ^{^} voln^*
68	67	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 $/\$ Σ^{^} voln^*
69	56, 65, 5, 68	fvmptd 6288	. . . . . . . . . . . . . . . . . . . 20 $/\$ Σ^{^} voln^*
70		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . . 23 voln^* voln^*
71	70	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . 22 Σ^{^} voln^* Σ^{^} voln^*
72	71	rabbidv 3189	. . . . . . . . . . . . . . . . . . . . 21 Σ^{^} voln^* Σ^{^} voln^*
73	72	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ Σ^{^} voln^* Σ^{^} voln^*
74		ovnsubaddlem1.e	. . . . . . . . . . . . . . . . . . . . . 22
75	74	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$
76		2nn 11185	. . . . . . . . . . . . . . . . . . . . . . . . 25
77	76	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24
78		nnnn0 11299	. . . . . . . . . . . . . . . . . . . . . . . 24
79	77, 78	nnexpcld 13030	. . . . . . . . . . . . . . . . . . . . . . 23
80	79	nnrpd 11870	. . . . . . . . . . . . . . . . . . . . . 22
81	80	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$
82	75, 81	rpdivcld 11889	. . . . . . . . . . . . . . . . . . . 20 $/\$
83		fvex 6201	. . . . . . . . . . . . . . . . . . . . . 22
84	83	rabex 4813	. . . . . . . . . . . . . . . . . . . . 21 Σ^{^} voln^*
85	84	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ Σ^{^} voln^*
86	69, 73, 82, 85	fvmptd 6288	. . . . . . . . . . . . . . . . . . 19 $/\$ Σ^{^} voln^*
87		ssrab2 3687	. . . . . . . . . . . . . . . . . . . 20 Σ^{^} voln^*
88	87	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ Σ^{^} voln^*
89	86, 88	eqsstrd 3639	. . . . . . . . . . . . . . . . . 18 $/\$
90		ovnsubaddlem1.i	. . . . . . . . . . . . . . . . . 18 $/\$
91	89, 90	sseldd 3604	. . . . . . . . . . . . . . . . 17 $/\$
92	54, 91	sseldd 3604	. . . . . . . . . . . . . . . 16 $/\$
93		elmapfn 7880	. . . . . . . . . . . . . . . 16
94	92, 93	syl 17	. . . . . . . . . . . . . . 15 $/\$
95		elmapi 7879	. . . . . . . . . . . . . . . . . 18
96	92, 95	syl 17	. . . . . . . . . . . . . . . . 17 $/\$
97	96	ffvelrnda 6359	. . . . . . . . . . . . . . . 16 $/\$ $/\$
98	97	ralrimiva 2966	. . . . . . . . . . . . . . 15 $/\$
99	94, 98	jca 554	. . . . . . . . . . . . . 14 $/\$ $/\$
100	99	3adant3 1081	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
101		ffnfv 6388	. . . . . . . . . . . . 13 $/\$
102	100, 101	sylibr 224	. . . . . . . . . . . 12 $/\$ $/\$
103		simp3 1063	. . . . . . . . . . . 12 $/\$ $/\$
104	102, 103	ffvelrnd 6360	. . . . . . . . . . 11 $/\$ $/\$
105		elmapi 7879	. . . . . . . . . . 11
106	104, 105	syl 17	. . . . . . . . . 10 $/\$ $/\$
107	36, 42, 106	vtocl 3259	. . . . . . . . 9 $/\$ $/\$
108	30, 35, 107	vtocl 3259	. . . . . . . 8 $/\$ $/\$
109	17, 27, 29, 108	syl3anc 1326	. . . . . . 7 $/\$
110		id 22	. . . . . . . . . 10
111		fvex 6201	. . . . . . . . . . 11
112	111	a1i 11	. . . . . . . . . 10
113		ovnsubaddlem1.g	. . . . . . . . . . 11
114	113	fvmpt2 6291	. . . . . . . . . 10 $/\$
115	110, 112, 114	syl2anc 693	. . . . . . . . 9
116	115	adantl 482	. . . . . . . 8 $/\$
117	116	feq1d 6030	. . . . . . 7 $/\$
118	109, 117	mpbird 247	. . . . . 6 $/\$
119	16, 18, 19, 118	hoiprodcl2 40769	. . . . 5 $/\$
120	15, 119	sseldi 3601	. . . 4 $/\$
121	12, 14, 120	sge0xrclmpt 40645	. . 3 Σ^{^}
122		nfv 1843	. . . 4
123		0xr 10086	. . . . . 6
124	123	a1i 11	. . . . 5 $/\$
125		pnfxr 10092	. . . . . 6
126	125	a1i 11	. . . . 5 $/\$
127	1	adantr 481	. . . . . . . . 9 $/\$
128		ovnsubaddlem1.z	. . . . . . . . 9 $/\$ Σ^{^}
129	127, 7, 128	ovnval2b 40766	. . . . . . . 8 $/\$ voln^* inf
130		ovnsubaddlem1.n0	. . . . . . . . . . 11
131	130	neneqd 2799	. . . . . . . . . 10
132	131	iffalsed 4097	. . . . . . . . 9 inf inf
133	132	adantr 481	. . . . . . . 8 $/\$ inf inf
134	129, 133	eqtrd 2656	. . . . . . 7 $/\$ voln^* inf
135	128	a1i 11	. . . . . . . . . 10 $/\$ $/\$ Σ^{^}
136		sseq1 3626	. . . . . . . . . . . . . 14
137	136	anbi1d 741	. . . . . . . . . . . . 13 $/\$ Σ^{^} $/\$ Σ^{^}
138	137	rexbidv 3052	. . . . . . . . . . . 12 $/\$ Σ^{^} $/\$ Σ^{^}
139	138	rabbidv 3189	. . . . . . . . . . 11 $/\$ Σ^{^} $/\$ Σ^{^}
140	139	adantl 482	. . . . . . . . . 10 $/\$ $/\$ $/\$ Σ^{^} $/\$ Σ^{^}
141		xrex 11829	. . . . . . . . . . . 12
142	141	rabex 4813	. . . . . . . . . . 11 $/\$ Σ^{^}
143	142	a1i 11	. . . . . . . . . 10 $/\$ $/\$ Σ^{^}
144	135, 140, 5, 143	fvmptd 6288	. . . . . . . . 9 $/\$ $/\$ Σ^{^}
145		ssrab2 3687	. . . . . . . . . 10 $/\$ Σ^{^}
146	145	a1i 11	. . . . . . . . 9 $/\$ $/\$ Σ^{^}
147	144, 146	eqsstrd 3639	. . . . . . . 8 $/\$
148		infxrcl 12163	. . . . . . . 8 inf
149	147, 148	syl 17	. . . . . . 7 $/\$ inf
150	134, 149	eqeltrd 2701	. . . . . 6 $/\$ voln^*
151	74	rpred 11872	. . . . . . . . 9
152	151	adantr 481	. . . . . . . 8 $/\$
153		2re 11090	. . . . . . . . . . 11
154	153	a1i 11	. . . . . . . . . 10
155	154, 78	reexpcld 13025	. . . . . . . . 9
156	155	adantl 482	. . . . . . . 8 $/\$
157	154	recnd 10068	. . . . . . . . . 10
158		2ne0 11113	. . . . . . . . . . 11
159	158	a1i 11	. . . . . . . . . 10
160		nnz 11399	. . . . . . . . . 10
161	157, 159, 160	expne0d 13014	. . . . . . . . 9
162	161	adantl 482	. . . . . . . 8 $/\$
163	152, 156, 162	redivcld 10853	. . . . . . 7 $/\$
164	163	rexrd 10089	. . . . . 6 $/\$
165	150, 164	xaddcld 12131	. . . . 5 $/\$ voln^*
166	127, 7	ovncl 40781	. . . . . . 7 $/\$ voln^*
167		xrge0ge0 39563	. . . . . . 7 voln^* voln^*
168	166, 167	syl 17	. . . . . 6 $/\$ voln^*
169		0red 10041	. . . . . . . . 9 $/\$
170	82	rpgt0d 11875	. . . . . . . . 9 $/\$
171	169, 163, 170	ltled 10185	. . . . . . . 8 $/\$
172	163	ltpnfd 11955	. . . . . . . . 9 $/\$
173	164, 126, 172	xrltled 39486	. . . . . . . 8 $/\$
174	124, 126, 164, 171, 173	eliccxrd 39753	. . . . . . 7 $/\$
175	150, 174	xadd0ge 39536	. . . . . 6 $/\$ voln^* voln^*
176	124, 150, 165, 168, 175	xrletrd 11993	. . . . 5 $/\$ voln^*
177		pnfge 11964	. . . . . 6 voln^* voln^*
178	165, 177	syl 17	. . . . 5 $/\$ voln^*
179	124, 126, 165, 176, 178	eliccxrd 39753	. . . 4 $/\$ voln^*
180	122, 14, 179	sge0xrclmpt 40645	. . 3 Σ^{^} voln^*
181	43	a1i 11	. . . . . . . . . . . 12 $/\$
182		sseq1 3626	. . . . . . . . . . . . . 14
183	182	rabbidv 3189	. . . . . . . . . . . . 13
184	183	adantl 482	. . . . . . . . . . . 12 $/\$ $/\$
185	2	adantr 481	. . . . . . . . . . . . 13 $/\$
186	185, 27	ffvelrnd 6360	. . . . . . . . . . . 12 $/\$
187	48	rabex 4813	. . . . . . . . . . . . 13
188	187	a1i 11	. . . . . . . . . . . 12 $/\$
189	181, 184, 186, 188	fvmptd 6288	. . . . . . . . . . 11 $/\$
190		ssrab2 3687	. . . . . . . . . . . 12
191	190	a1i 11	. . . . . . . . . . 11 $/\$
192	189, 191	eqsstrd 3639	. . . . . . . . . 10 $/\$
193	55	a1i 11	. . . . . . . . . . . . . 14 $/\$ Σ^{^} voln^*
194		fveq2 6191	. . . . . . . . . . . . . . . . . . 19
195	194	eleq2d 2687	. . . . . . . . . . . . . . . . . 18
196		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20 voln^* voln^*
197	196	oveq1d 6665	. . . . . . . . . . . . . . . . . . 19 voln^* voln^*
198	197	breq2d 4665	. . . . . . . . . . . . . . . . . 18 Σ^{^} voln^* Σ^{^} voln^*
199	195, 198	anbi12d 747	. . . . . . . . . . . . . . . . 17 $/\$ Σ^{^} voln^* $/\$ Σ^{^} voln^*
200	199	rabbidva2 3186	. . . . . . . . . . . . . . . 16 Σ^{^} voln^* Σ^{^} voln^*
201	200	mpteq2dv 4745	. . . . . . . . . . . . . . 15 Σ^{^} voln^* Σ^{^} voln^*
202	201	adantl 482	. . . . . . . . . . . . . 14 $/\$ $/\$ Σ^{^} voln^* Σ^{^} voln^*
203	66	mptex 6486	. . . . . . . . . . . . . . 15 Σ^{^} voln^*
204	203	a1i 11	. . . . . . . . . . . . . 14 $/\$ Σ^{^} voln^*
205	193, 202, 186, 204	fvmptd 6288	. . . . . . . . . . . . 13 $/\$ Σ^{^} voln^*
206		oveq2 6658	. . . . . . . . . . . . . . . 16 voln^* voln^*
207	206	breq2d 4665	. . . . . . . . . . . . . . 15 Σ^{^} voln^* Σ^{^} voln^*
208	207	rabbidv 3189	. . . . . . . . . . . . . 14 Σ^{^} voln^* Σ^{^} voln^*
209	208	adantl 482	. . . . . . . . . . . . 13 $/\$ $/\$ Σ^{^} voln^* Σ^{^} voln^*
210	17, 74	syl 17	. . . . . . . . . . . . . 14 $/\$
211		2rp 11837	. . . . . . . . . . . . . . . 16
212	211	a1i 11	. . . . . . . . . . . . . . 15 $/\$
213	27	nnzd 11481	. . . . . . . . . . . . . . 15 $/\$
214	212, 213	rpexpcld 13032	. . . . . . . . . . . . . 14 $/\$
215	210, 214	rpdivcld 11889	. . . . . . . . . . . . 13 $/\$
216		fvex 6201	. . . . . . . . . . . . . . 15
217	216	rabex 4813	. . . . . . . . . . . . . 14 Σ^{^} voln^*
218	217	a1i 11	. . . . . . . . . . . . 13 $/\$ Σ^{^} voln^*
219	205, 209, 215, 218	fvmptd 6288	. . . . . . . . . . . 12 $/\$ Σ^{^} voln^*
220		ssrab2 3687	. . . . . . . . . . . . 13 Σ^{^} voln^*
221	220	a1i 11	. . . . . . . . . . . 12 $/\$ Σ^{^} voln^*
222	219, 221	eqsstrd 3639	. . . . . . . . . . 11 $/\$
223	37	anbi2d 740	. . . . . . . . . . . . . 14 $/\$ $/\$
224		fveq2 6191	. . . . . . . . . . . . . . . . 17
225	224	fveq2d 6195	. . . . . . . . . . . . . . . 16
226		oveq2 6658	. . . . . . . . . . . . . . . . 17
227	226	oveq2d 6666	. . . . . . . . . . . . . . . 16
228	225, 227	fveq12d 6197	. . . . . . . . . . . . . . 15
229	39, 228	eleq12d 2695	. . . . . . . . . . . . . 14
230	223, 229	imbi12d 334	. . . . . . . . . . . . 13 $/\$ $/\$
231	36, 230, 90	vtocl 3259	. . . . . . . . . . . 12 $/\$
232	17, 27, 231	syl2anc 693	. . . . . . . . . . 11 $/\$
233	222, 232	sseldd 3604	. . . . . . . . . 10 $/\$
234	192, 233	sseldd 3604	. . . . . . . . 9 $/\$
235		elmapfn 7880	. . . . . . . . 9
236	234, 235	syl 17	. . . . . . . 8 $/\$
237		elmapi 7879	. . . . . . . . . . 11
238	234, 237	syl 17	. . . . . . . . . 10 $/\$
239	238	ffvelrnda 6359	. . . . . . . . 9 $/\$ $/\$
240	239	ralrimiva 2966	. . . . . . . 8 $/\$
241	236, 240	jca 554	. . . . . . 7 $/\$ $/\$
242		ffnfv 6388	. . . . . . 7 $/\$
243	241, 242	sylibr 224	. . . . . 6 $/\$
244	243, 29	ffvelrnd 6360	. . . . 5 $/\$
245	244, 113	fmptd 6385	. . . 4
246		simpl 473	. . . . . . . . 9 $/\$
247	90, 86	eleqtrd 2703	. . . . . . . . . 10 $/\$ Σ^{^} voln^*
248	87, 247	sseldi 3601	. . . . . . . . 9 $/\$
249		simp3 1063	. . . . . . . . . . . 12 $/\$ $/\$
250	51	3adant3 1081	. . . . . . . . . . . 12 $/\$ $/\$
251	249, 250	eleqtrd 2703	. . . . . . . . . . 11 $/\$ $/\$
252		fveq1 6190	. . . . . . . . . . . . . . . . 17
253	252	coeq2d 5284	. . . . . . . . . . . . . . . 16
254	253	fveq1d 6193	. . . . . . . . . . . . . . 15
255	254	ixpeq2dv 7924	. . . . . . . . . . . . . 14
256	255	iuneq2d 4547	. . . . . . . . . . . . 13
257	256	sseq2d 3633	. . . . . . . . . . . 12
258	257	elrab 3363	. . . . . . . . . . 11 $/\$
259	251, 258	sylib 208	. . . . . . . . . 10 $/\$ $/\$ $/\$
260	259	simprd 479	. . . . . . . . 9 $/\$ $/\$
261	246, 4, 248, 260	syl3anc 1326	. . . . . . . 8 $/\$
262		f1ofo 6144	. . . . . . . . . . . . . 14
263	20, 262	syl 17	. . . . . . . . . . . . 13
264	263	ad2antrr 762	. . . . . . . . . . . 12 $/\$ $/\$
265		opelxpi 5148	. . . . . . . . . . . . 13 $/\$
266	4, 265	sylan 488	. . . . . . . . . . . 12 $/\$ $/\$
267		foelrni 6244	. . . . . . . . . . . 12 $/\$
268	264, 266, 267	syl2anc 693	. . . . . . . . . . 11 $/\$ $/\$
269		nfv 1843	. . . . . . . . . . . 12 $/\$ $/\$
270		nfre1 3005	. . . . . . . . . . . 12
271		simpl 473	. . . . . . . . . . . . . . . . 17 $/\$
272		fveq2 6191	. . . . . . . . . . . . . . . . . . 19
273		vex 3203	. . . . . . . . . . . . . . . . . . . . 21
274		vex 3203	. . . . . . . . . . . . . . . . . . . . 21
275		op1stg 7180	. . . . . . . . . . . . . . . . . . . . 21 $/\$
276	273, 274, 275	mp2an 708	. . . . . . . . . . . . . . . . . . . 20
277	276	a1i 11	. . . . . . . . . . . . . . . . . . 19
278	272, 277	eqtrd 2656	. . . . . . . . . . . . . . . . . 18
279	278	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$
280	271, 279	jca 554	. . . . . . . . . . . . . . . 16 $/\$ $/\$
281		fveq2 6191	. . . . . . . . . . . . . . . . . . 19
282	281	fveq2d 6195	. . . . . . . . . . . . . . . . . 18
283	282	eqeq1d 2624	. . . . . . . . . . . . . . . . 17
284	283	elrab 3363	. . . . . . . . . . . . . . . 16 $/\$
285	280, 284	sylibr 224	. . . . . . . . . . . . . . 15 $/\$
286	285	3adant1 1079	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
287	271, 115	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$
288	278	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . 22
289	273, 274	op2ndd 7179	. . . . . . . . . . . . . . . . . . . . . 22
290	288, 289	fveq12d 6197	. . . . . . . . . . . . . . . . . . . . 21
291	290	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$
292	287, 291	eqtr2d 2657	. . . . . . . . . . . . . . . . . . 19 $/\$
293	292	coeq2d 5284	. . . . . . . . . . . . . . . . . 18 $/\$
294	293	fveq1d 6193	. . . . . . . . . . . . . . . . 17 $/\$
295	294	ixpeq2dv 7924	. . . . . . . . . . . . . . . 16 $/\$
296		eqimss 3657	. . . . . . . . . . . . . . . 16
297	295, 296	syl 17	. . . . . . . . . . . . . . 15 $/\$
298	297	3adant1 1079	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
299		rspe 3003	. . . . . . . . . . . . . 14 $/\$
300	286, 298, 299	syl2anc 693	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
301	300	3exp 1264	. . . . . . . . . . . 12 $/\$ $/\$
302	269, 270, 301	rexlimd 3026	. . . . . . . . . . 11 $/\$ $/\$
303	268, 302	mpd 15	. . . . . . . . . 10 $/\$ $/\$
304	303	ralrimiva 2966	. . . . . . . . 9 $/\$
305		iunss2 4565	. . . . . . . . 9
306	304, 305	syl 17	. . . . . . . 8 $/\$
307	261, 306	sstrd 3613	. . . . . . 7 $/\$
308		ssrab2 3687	. . . . . . . . 9
309		iunss1 4532	. . . . . . . . 9
310	308, 309	ax-mp 5	. . . . . . . 8
311	310	a1i 11	. . . . . . 7 $/\$
312	307, 311	sstrd 3613	. . . . . 6 $/\$
313	312	ralrimiva 2966	. . . . 5
314		iunss 4561	. . . . 5
315	313, 314	sylibr 224	. . . 4
316	1, 130, 19, 245, 315	ovnlecvr 40772	. . 3 voln^* Σ^{^}
317	116	fveq2d 6195	. . . . . . 7 $/\$
318	317	mpteq2dva 4744	. . . . . 6
319	318	fveq2d 6195	. . . . 5 Σ^{^} Σ^{^}
320		nfv 1843	. . . . . 6
321		fveq2 6191	. . . . . . . . 9
322	321	fveq2d 6195	. . . . . . . 8
323		fveq2 6191	. . . . . . . 8
324	322, 323	fveq12d 6197	. . . . . . 7
325	324	fveq2d 6195	. . . . . 6
326		eqidd 2623	. . . . . 6 $/\$
327		nfv 1843	. . . . . . . 8 $/\$
328	1	adantr 481	. . . . . . . 8 $/\$
329		simpl 473	. . . . . . . . 9 $/\$
330		xp1st 7198	. . . . . . . . . 10
331	330	adantl 482	. . . . . . . . 9 $/\$
332		xp2nd 7199	. . . . . . . . . 10
333	332	adantl 482	. . . . . . . . 9 $/\$
334		fvex 6201	. . . . . . . . . 10
335		eleq1 2689	. . . . . . . . . . . 12
336	335	3anbi3d 1405	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
337		fveq2 6191	. . . . . . . . . . . 12
338	337	feq1d 6030	. . . . . . . . . . 11
339	336, 338	imbi12d 334	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
340		fvex 6201	. . . . . . . . . . 11
341		eleq1 2689	. . . . . . . . . . . . 13
342	341	3anbi2d 1404	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
343		fveq2 6191	. . . . . . . . . . . . . 14
344	343	fveq1d 6193	. . . . . . . . . . . . 13
345	344	feq1d 6030	. . . . . . . . . . . 12
346	342, 345	imbi12d 334	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
347	340, 346, 106	vtocl 3259	. . . . . . . . . 10 $/\$ $/\$
348	334, 339, 347	vtocl 3259	. . . . . . . . 9 $/\$ $/\$
349	329, 331, 333, 348	syl3anc 1326	. . . . . . . 8 $/\$
350	327, 328, 19, 349	hoiprodcl2 40769	. . . . . . 7 $/\$
351	15, 350	sseldi 3601	. . . . . 6 $/\$
352	320, 12, 325, 14, 20, 326, 351	sge0f1o 40599	. . . . 5 Σ^{^} Σ^{^}
353	319, 352	eqtr4d 2659	. . . 4 Σ^{^} Σ^{^}
354		nfv 1843	. . . . . . 7
355	273, 274	op1std 7178	. . . . . . . . . 10
356	355	fveq2d 6195	. . . . . . . . 9
357	273, 274	op2ndd 7179	. . . . . . . . 9
358	356, 357	fveq12d 6197	. . . . . . . 8
359	358	fveq2d 6195	. . . . . . 7
360		nfv 1843	. . . . . . . . . 10 $/\$ $/\$
361	127	adantr 481	. . . . . . . . . 10 $/\$ $/\$
362	97, 105	syl 17	. . . . . . . . . 10 $/\$ $/\$
363	360, 361, 19, 362	hoiprodcl2 40769	. . . . . . . . 9 $/\$ $/\$
364	15, 363	sseldi 3601	. . . . . . . 8 $/\$ $/\$
365	364	3impa 1259	. . . . . . 7 $/\$ $/\$
366	354, 359, 14, 14, 365	sge0xp 40646	. . . . . 6 Σ^{^} Σ^{^} Σ^{^}
367	366	eqcomd 2628	. . . . 5 Σ^{^} Σ^{^} Σ^{^}
368	13	a1i 11	. . . . . . 7 $/\$
369		eqid 2622	. . . . . . . 8
370	364, 369	fmptd 6385	. . . . . . 7 $/\$
371	368, 370	sge0cl 40598	. . . . . 6 $/\$ Σ^{^}
372		fveq1 6190	. . . . . . . . . . . . 13
373	372	fveq2d 6195	. . . . . . . . . . . 12
374	373	mpteq2dv 4745	. . . . . . . . . . 11
375	374	fveq2d 6195	. . . . . . . . . 10 Σ^{^} Σ^{^}
376	375	breq1d 4663	. . . . . . . . 9 Σ^{^} voln^* Σ^{^} voln^*
377	376	elrab 3363	. . . . . . . 8 Σ^{^} voln^* $/\$ Σ^{^} voln^*
378	247, 377	sylib 208	. . . . . . 7 $/\$ $/\$ Σ^{^} voln^*
379	378	simprd 479	. . . . . 6 $/\$ Σ^{^} voln^*
380	122, 14, 371, 179, 379	sge0lempt 40627	. . . . 5 Σ^{^} Σ^{^} Σ^{^} voln^*
381	367, 380	eqbrtrd 4675	. . . 4 Σ^{^} Σ^{^} voln^*
382	353, 381	eqbrtrd 4675	. . 3 Σ^{^} Σ^{^} voln^*
383	11, 121, 180, 316, 382	xrletrd 11993	. 2 voln^* Σ^{^} voln^*
384	122, 14, 166, 174	sge0xadd 40652	. . 3 Σ^{^} voln^* Σ^{^} voln^*Σ^{^}
385	123	a1i 11	. . . . . 6
386	125	a1i 11	. . . . . 6
387	151	rexrd 10089	. . . . . 6
388	74	rpge0d 11876	. . . . . 6
389	151	ltpnfd 11955	. . . . . 6
390	385, 386, 387, 388, 389	elicod 12224	. . . . 5
391	390	sge0ad2en 40648	. . . 4 Σ^{^}
392	391	oveq2d 6666	. . 3 Σ^{^} voln^Σ^{^} Σ^{^} voln^
393	384, 392	eqtrd 2656	. 2 Σ^{^} voln^* Σ^{^} voln^*
394	383, 393	breqtrd 4679	1 voln^* Σ^{^} voln^*

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 384 $/\$ w3a 1037

wceq 1483

wcel 1990

wne 2794

wral 2912

wrex 2913

crab 2916

cvv 3200

wss 3574

c0 3915

cif 4086

cpw 4158

cop 4183

ciun 4520 class class class wbr 4653

cmpt 4729

cxp 5112

ccom 5118

wfn 5883

wf 5884

wfo 5886

wf1o 5887

cfv 5888 (class class class)co 6650

c1st 7166

c2nd 7167

cmap 7857

cixp 7908

cfn 7955 infcinf 8347

cr 9935

cc0 9936

cpnf 10071

cxr 10073

clt 10074

cle 10075

cdiv 10684

cn 11020

c2 11070

crp 11832

cxad 11944

cico 12177

cicc 12178

cexp 12860

cprod 14635

cvol 23232 Σ^{^}csumge0 40579 voln^*covoln 40750

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-ac2 9285 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014 ax-addf 10015 ax-mulf 10016

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-disj 4621 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-om 7066 df-1st 7168 df-2nd 7169 df-tpos 7352 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-ixp 7909 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fi 8317 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-acn 8768 df-ac 8939 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-z 11378 df-dec 11494 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ioo 12179 df-ico 12181 df-icc 12182 df-fz 12327 df-fzo 12466 df-fl 12593 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-clim 14219 df-rlim 14220 df-sum 14417 df-prod 14636 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-sets 15864 df-ress 15865 df-plusg 15954 df-mulr 15955 df-starv 15956 df-tset 15960 df-ple 15961 df-ds 15964 df-unif 15965 df-rest 16083 df-0g 16102 df-topgen 16104 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-grp 17425 df-minusg 17426 df-subg 17591 df-cmn 18195 df-abl 18196 df-mgp 18490 df-ur 18502 df-ring 18549 df-cring 18550 df-oppr 18623 df-dvdsr 18641 df-unit 18642 df-invr 18672 df-dvr 18683 df-drng 18749 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-cnfld 19747 df-top 20699 df-topon 20716 df-bases 20750 df-cmp 21190 df-ovol 23233 df-vol 23234 df-sumge0 40580 df-ovoln 40751

This theorem is referenced by: ovnsubaddlem2 40785

W3C validator